tests/lean/dsimpZetaIssue.lean.expected.out - third_party/github.com/leanprover/lean4 - Git at Google


            
            ⊢ let x := 0;

            
              x + 5 = 5

            
            y : Nat

            
            ⊢ 0 + y = y

            
            y : Nat

            
            ⊢ let x := 0;

            
              x + y = y

            
            y : Nat

            
            ⊢ 0 + y = y
	⊢ let x := 0;
	x + 5 = 5
	y : Nat
	⊢ 0 + y = y
	y : Nat
	⊢ let x := 0;
	x + y = y
	y : Nat
	⊢ 0 + y = y