proof1 : HTProof initCond program termCond
proof1 =
  SeqRule {!$\lambda$! e !$\rightarrow$! true} ( PrimRule empty-case )
    $ SeqRule {!$\lambda$! e !$\rightarrow$!  Equal (varn e) 10} ( PrimRule lemma1   )
    $ WeakeningRule {!$\lambda$! e !$\rightarrow$! (Equal (varn e) 10) !$\wedge$! (Equal (vari e) 0)}  lemma2 (
      WhileRule {_} {!$\lambda$! e !$\rightarrow$! Equal ((varn e) + (vari e)) 10}
        $ SeqRule (PrimRule {!$\lambda$! e !$\rightarrow$!  whileInv e  !$\wedge$! lt zero (varn e) } lemma3 )
        $ PrimRule {whileInv!$\prime$!} {_} {whileInv}  lemma4 ) lemma5