tests/elab/issue7826a.lean - third_party/github.com/leanprover/lean4 - Git at Google


            
            example (a b : Nat) (h : a = b):

            
              (let _ : id Bool := true; a) = (let _ : Bool := true; b) := by

            
              simp -zeta -zetaDelta [h]
	example (a b : Nat) (h : a = b):
	(let _ : id Bool := true; a) = (let _ : Bool := true; b) := by
	simp -zeta -zetaDelta [h]