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


            
            axiom A : Nat

            
            axiom B : Nat

            
            axiom equality : A = B


            example : A = 3 -> B = 3 := by

            
              intro h

            
              rewrite [equality] at *
	axiom A : Nat
	axiom B : Nat
	axiom equality : A = B

	example : A = 3 -> B = 3 := by
	intro h
	rewrite [equality] at *