let p, q be ZF-formula; :: thesis: Free (p => q) = (Free p) \/ (Free q)
thus Free (p => q) = Free (p '&' ('not' q)) by Th60
.= (Free p) \/ (Free ('not' q)) by Th61
.= (Free p) \/ (Free q) by Th60 ; :: thesis: verum