take Goto 0 ; :: thesis: ( Goto 0 is halt-free & Goto 0 is good )
thus ( Goto 0 is halt-free & Goto 0 is good ) ; :: thesis: verum