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'} {_} {whileInv}  lemma4 ) lemma5