| x : Nat | |
| | id (twice (id x)) | |
| x : Nat | |
| | id x | |
| x : Nat | |
| | x | |
| x : Nat | |
| | id (twice x) | |
| convInConv.lean:15:8-15:12: warning: declaration uses 'sorry' | |
| y : Nat | |
| | (fun x => x + y = 0) = fun x => False | |
| y : Nat | |
| | fun x => x + y = 0 | |
| case h | |
| y x : Nat | |
| | y + x = 0 | |
| y : Nat | |
| | (fun x => y + x = 0) = fun x => False | |
| y : Nat | |
| ⊢ (fun x => y + x = 0) = fun x => False |