Soundness : {bPre : Cond} !$\rightarrow$! {cm : Comm} !$\rightarrow$! {bPost : Cond} !$\rightarrow$!
            HTProof bPre cm bPost !$\rightarrow$! Satisfies bPre cm bPost
Soundness (PrimRule {bPre} {cm} {bPost} pr) s1 s2 q1 q2
  = axiomValid bPre cm bPost pr s1 s2 q1 q2
Soundness {.bPost} {.Skip} {bPost} (SkipRule .bPost) s1 s2 q1 q2
  = substId1 State {Level.zero} {State} {s1} {s2} (proj!$\_{2}$! q2) (SemCond bPost) q1
Soundness {bPre} {.Abort} {bPost} (AbortRule .bPre .bPost) s1 s2 q1 ()
Soundness (WeakeningRule {bPre} {bPre!$\prime$!} {cm} {bPost!$\prime$!} {bPost} tautPre pr tautPost)
          s1 s2 q1 q2
  = let hyp : Satisfies bPre!$\prime$! cm bPost!$\prime$!
        hyp = Soundness pr
    in tautValid bPost!$\prime$! bPost tautPost s2 (hyp s1 s2 (tautValid bPre bPre!$\prime$! tautPre s1 q1) q2)
Soundness (SeqRule {bPre} {cm1} {bMid} {cm2} {bPost} pr1 pr2)
           s1 s2 q1 q2
  = let hyp1 : Satisfies bPre cm1 bMid
        hyp1 = Soundness pr1
        hyp2 : Satisfies bMid cm2 bPost
        hyp2 = Soundness pr2
    in hyp2 (proj!$\_{1}$! q2) s2 (hyp1 s1 (proj!$\_{1}$! q2) q1 (proj!$\_{1}$! (proj!$\_{2}$! q2))) (proj!$\_{2}$! (proj!$\_{2}$! q2))
Soundness (IfRule {cmThen} {cmElse} {bPre} {bPost} {b} pThen pElse)
          s1 s2 q1 q2
  = let hypThen : Satisfies (bPre !$\wedge$! b) cmThen bPost
        hypThen = Soundness pThen
        hypElse : Satisfies (bPre !$\wedge$! neg b) cmElse bPost
        hypElse = Soundness pElse
        rThen : RelOpState.comp (RelOpState.delta (SemCond b))
                  (SemComm cmThen) s1 s2 !$\rightarrow$! SemCond bPost s2
        rThen = !$\lambda$! h !$\rightarrow$! hypThen s1 s2 ((proj!$\_{2}$! (respAnd bPre b s1)) (q1 , proj!$\_{1}$! t1))
          (proj!$\_{2}$! ((proj!$\_{2}$! (RelOpState.deltaRestPre (SemCond b) (SemComm cmThen) s1 s2)) h))
        rElse : RelOpState.comp (RelOpState.delta (NotP (SemCond b)))
                  (SemComm cmElse) s1 s2 !$\rightarrow$! SemCond bPost s2
        rElse = !$\lambda$! h !$\rightarrow$!
                  let t10 : (NotP (SemCond b) s1) !$\times$! (SemComm cmElse s1 s2)
                      t10 = proj!$\_{2}$! (RelOpState.deltaRestPre
                                  (NotP (SemCond b)) (SemComm cmElse) s1 s2) h
                  in hypElse s1 s2 (proj!$\_{2}$! (respAnd bPre (neg b) s1)
                             (q1 , (proj!$\_{2}$! (respNeg b s1) (proj!$\_{1}$! t10)))) (proj!$\_{2}$! t10)
    in when rThen rElse q2
Soundness (WhileRule {cm!$\prime$!} {bInv} {b} pr) s1 s2 q1 q2
  = proj!$\_{2}$! (respAnd bInv (neg b) s2)
          (lem1 (proj!$\_{1}$! q2) s2 (proj!$\_{1}$! t15) , proj!$\_{2}$! (respNeg b s2) (proj!$\_{2}$! t15))
    where
      hyp : Satisfies (bInv !$\wedge$! b) cm!$\prime$! bInv
      hyp = Soundness pr
      Rel1 : !$\mathbb{N}$! !$\rightarrow$! Rel State (Level.zero)
      Rel1 = !$\lambda$! m !$\rightarrow$!
               RelOpState.repeat
                 m
                 (RelOpState.comp (RelOpState.delta (SemCond b))
                                  (SemComm cm!$\prime$!))
      t15 : (Rel1 (proj!$\_{1}$! q2) s1 s2) !$\times$! (NotP (SemCond b) s2)
      t15 = proj!$\_{2}$! (RelOpState.deltaRestPost
        (NotP (SemCond b)) (Rel1 (proj!$\_{1}$! q2)) s1 s2) (proj!$\_{2}$! q2)
      lem1 : (m : !$\mathbb{N}$!) !$\rightarrow$! (ss2 : State) !$\rightarrow$! Rel1 m s1 ss2 !$\rightarrow$! SemCond bInv ss2
      lem1 zero ss2 h = substId1 State (proj!$\_{2}$! h) (SemCond bInv) q1
      lem1 (suc n) ss2 h
    = let hyp2 : (z : State) !$\rightarrow$! Rel1 (proj!$\_{1}$! q2) s1 z !$\rightarrow$!
                     SemCond bInv z
              hyp2 = lem1 n
              t22 : (SemCond b (proj!$\_{1}$! h)) !$\times$! (SemComm cm!$\prime$! (proj!$\_{1}$! h) ss2)
              t22 = proj!$\_{2}$! (RelOpState.deltaRestPre (SemCond b) (SemComm cm!$\prime$!) (proj!$\_{1}$! h) ss2)
                    (proj!$\_{2}$! (proj!$\_{2}$! h))
              t23 : SemCond (bInv !$\wedge$! b) (proj!$\_{1}$! h)
              t23 = proj!$\_{2}$! (respAnd bInv b (proj!$\_{1}$! h))
                (hyp2 (proj!$\_{1}$! h) (proj!$\_{1}$! (proj!$\_{2}$! h)) , proj!$\_{1}$! t22)
      in hyp (proj!$\_{1}$! h) ss2 t23 (proj!$\_{2}$! t22)