| k : Nat | |
| h : 11 = k | |
| this : f 10 = 11 | |
| ⊢ 11 = k | |
| k y : Nat | |
| h : | |
| let x := y; | |
| f x = k | |
| ⊢ f y = k | |
| g : Nat → Nat | |
| y : Nat | |
| h : | |
| let x := y; | |
| g x = 0 + x | |
| ⊢ g y = 0 + y | |
| g : Nat → Nat | |
| y : Nat | |
| h : | |
| let x := y; | |
| let z := y + 1; | |
| g x = 0 + z | |
| ⊢ g y = y + 1 | |
| g : Nat → Nat | |
| y : Nat | |
| h : | |
| let x := y; | |
| let z := y + 1; | |
| g x = z | |
| ⊢ g y = y + 1 |