data HTProof : Cond !$\rightarrow$! Comm !$\rightarrow$! Cond !$\rightarrow$! Set where
  PrimRule : {bPre : Cond} !$\rightarrow$! {pcm : PrimComm} !$\rightarrow$! {bPost : Cond} !$\rightarrow$!
             (pr : Axiom bPre pcm bPost) !$\rightarrow$!
             HTProof bPre (PComm pcm) bPost
  SkipRule : (b : Cond) !$\rightarrow$! HTProof b Skip b
  AbortRule : (bPre : Cond) !$\rightarrow$! (bPost : Cond) !$\rightarrow$!
              HTProof bPre Abort bPost
  WeakeningRule : {bPre : Cond} !$\rightarrow$! {bPre!$\prime$! : Cond} !$\rightarrow$! {cm : Comm} !$\rightarrow$!
                {bPost!$\prime$! : Cond} !$\rightarrow$! {bPost : Cond} !$\rightarrow$!
                Tautology bPre bPre!$\prime$! !$\rightarrow$!
                HTProof bPre!$\prime$! cm bPost!$\prime$! !$\rightarrow$!
                Tautology bPost!$\prime$! bPost !$\rightarrow$!
                HTProof bPre cm bPost
  SeqRule : {bPre : Cond} !$\rightarrow$! {cm1 : Comm} !$\rightarrow$! {bMid : Cond} !$\rightarrow$!
            {cm2 : Comm} !$\rightarrow$! {bPost : Cond} !$\rightarrow$!
            HTProof bPre cm1 bMid !$\rightarrow$!
            HTProof bMid cm2 bPost !$\rightarrow$!
            HTProof bPre (Seq cm1 cm2) bPost
  IfRule : {cmThen : Comm} !$\rightarrow$! {cmElse : Comm} !$\rightarrow$!
           {bPre : Cond} !$\rightarrow$! {bPost : Cond} !$\rightarrow$!
           {b : Cond} !$\rightarrow$!
           HTProof (bPre !$\wedge$! b) cmThen bPost !$\rightarrow$!
           HTProof (bPre !$\wedge$! neg b) cmElse bPost !$\rightarrow$!
           HTProof bPre (If b cmThen cmElse) bPost
  WhileRule : {cm : Comm} !$\rightarrow$! {bInv : Cond} !$\rightarrow$! {b : Cond} !$\rightarrow$!
              HTProof (bInv !$\wedge$! b) cm bInv !$\rightarrow$!
              HTProof bInv (While b cm) (bInv !$\wedge$! neg b)