| case intro | |
| n : Nat | |
| m : Nat := n | |
| a : Nat | |
| e : id a = m | |
| ⊢ 0 + n = n | |
| case intro | |
| a : Nat | |
| m : Nat := id a | |
| ⊢ 0 + id a = id a | |
| case intro | |
| n : Nat | |
| m : Nat := n | |
| a : Nat | |
| e : m = id a | |
| ⊢ 0 + n = n | |
| case intro | |
| n : Nat | |
| m : Nat := n | |
| ⊢ 0 + n = n | |
| substlet.lean:25:2-25:9: error: tactic 'subst' failed, variable 'v' is a let-declaration | |
| n : Nat | |
| h : n = 0 | |
| m : Nat := n + 1 | |
| v : Nat := m + 1 | |
| this : v = n + 2 | |
| ⊢ 0 + n = 0 |