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


            
            example (h : ∀ x, x + 1 = x.succ) : (x + 1) + 1 = 1 + (x + 1) := by

            
              rewrite [h]

            
              done
	example (h : ∀ x, x + 1 = x.succ) : (x + 1) + 1 = 1 + (x + 1) := by
	rewrite [h]
	done