1 tt $f term t 2 tze$a term 0 3 1,2 tpl $a term ( t + 0 ) 4 tt$f term t 5 3,4 weq $a wff ( t + 0 ) = t 6 tt$f term t 7 tt $f term t 8 6,7 weq$a wff t = t 9 tt $f term t 10 9 a2$a |- ( t + 0 ) = t 11 tt $f term t 12 tze$a term 0 13 11,12 tpl $a term ( t + 0 ) 14 tt$f term t 15 13,14 weq $a wff ( t + 0 ) = t 16 tt$f term t 17 tze $a term 0 18 16,17 tpl$a term ( t + 0 ) 19 tt $f term t 20 18,19 weq$a wff ( t + 0 ) = t 21 tt $f term t 22 tt$f term t 23 21,22 weq $a wff t = t 24 20,23 wim$a wff ( ( t + 0 ) = t -> t = t ) 25 tt $f term t 26 25 a2$a |- ( t + 0 ) = t 27 tt $f term t 28 tze$a term 0 29 27,28 tpl $a term ( t + 0 ) 30 tt$f term t 31 tt $f term t 32 29,30,31 a1$a |- ( ( t + 0 ) = t -> ( ( t + 0 ) = t -> t = t ) ) 33 15,24,26,32 mp $a |- ( ( t + 0 ) = t -> t = t ) 34 5,8,10,33 mp$a |- t = t