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@$\text{2}$@ q2) (SemCond bPost) q1
Soundness {bPre} {.Abort} {bPost} (AbortRule .bPre .bPost) s1 s2 q1 ()
Soundness (WeakeningRule {bPre} {bPre'} {cm} {bPost'} {bPost} tautPre pr tautPost)
          s1 s2 q1 q2
  = let hyp : Satisfies bPre' cm bPost'
        hyp = Soundness pr
        r1 : SemCond bPre' s1
        r1 = tautValid bPre bPre' tautPre s1 q1
        r2 : SemCond bPost' s2
        r2 = hyp s1 s2 r1 q2
    in tautValid bPost' bPost tautPost s2 r2
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
        sMid : State
        sMid = proj@$\text{1}$@ q2
        r1 : SemComm cm1 s1 sMid @$\times$@ SemComm cm2 sMid s2
        r1 = proj@$\text{2}$@ q2
        r2 : SemComm cm1 s1 sMid
        r2 = proj@$\text{1}$@ r1
        r3 : SemComm cm2 sMid s2
        r3 = proj@$\text{2}$@ r1
        r4 : SemCond bMid sMid
        r4 = hyp1 s1 sMid q1 r2
    in hyp2 sMid s2 r4 r3
Soundness (IfRule {cmThen} {cmElse} {bPre} {bPost} {b} pThen pElse)
          s1 s2 q1 q2
  = let hypThen : Satisfies (bPre /\ b) cmThen bPost
        hypThen = Soundness pThen
        hypElse : Satisfies (bPre /\ 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$@
                  let t1 : SemCond b s1 @$\times$@ SemComm cmThen s1 s2
                      t1 = (proj@$\text{2}$@ (RelOpState.deltaRestPre
                                     (SemCond b)
                                     (SemComm cmThen) s1 s2)) h
                      t2 : SemCond (bPre /\ b) s1
                      t2 = (proj@$\text{2}$@ (respAnd bPre b s1))
                           (q1 , proj@$\text{1}$@ t1)
                  in hypThen s1 s2 t2 (proj@$\text{2}$@ t1)
        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@$\text{2}$@ (RelOpState.deltaRestPre
                                    (NotP (SemCond b)) (SemComm cmElse) s1 s2)
                            h
                      t6 : SemCond (neg b) s1
                      t6 = proj@$\text{2}$@ (respNeg b s1) (proj@$\text{1}$@ t10)
                      t7 : SemComm cmElse s1 s2
                      t7 = proj@$\text{2}$@ t10
                      t8 : SemCond (bPre /\ neg b) s1
                      t8 = proj@$\text{2}$@ (respAnd bPre (neg b) s1)
                           (q1 , t6)
                  in hypElse s1 s2 t8 t7
    in when rThen rElse q2
Soundness (WhileRule {cm'} {bInv} {b} pr) s1 s2 q1 q2
  = proj@$\text{2}$@ (respAnd bInv (neg b) s2) t20
    where
      hyp : Satisfies (bInv /\ b) cm' bInv
      hyp = Soundness pr
      n : $mathbb{N}$
      n = proj@$\text{1}$@ q2
      Rel1 : $mathbb{N}$ @$\rightarrow$@ Rel State (Level.zero)
      Rel1 = @$\lambda$@ m @$\rightarrow$@
               RelOpState.repeat
                 m
                 (RelOpState.comp (RelOpState.delta (SemCond b))
                                  (SemComm cm'))
      t1 : RelOpState.comp
             (Rel1 n)
             (RelOpState.delta (NotP (SemCond b))) s1 s2
      t1 = proj@$\text{2}$@ q2
      t15 : (Rel1 n s1 s2) @$\times$@ (NotP (SemCond b) s2)
      t15 = proj@$\text{2}$@ (RelOpState.deltaRestPost
                    (NotP (SemCond b)) (Rel1 n) s1 s2)
              t1
      t16 : Rel1 n s1 s2
      t16 = proj@$\text{1}$@ t15
      t17 : NotP (SemCond b) s2
      t17 = proj@$\text{2}$@ t15
      lem1 : (m : $mathbb{N}$) @$\rightarrow$@ (ss2 : State) @$\rightarrow$@ Rel1 m s1 ss2 @$\rightarrow$@
             SemCond bInv ss2
      lem1 $mathbb{N}$.zero ss2 h
        = substId1 State (proj@$\text{2}$@ h) (SemCond bInv) q1
      lem1 ($mathbb{N}$.suc n) ss2 h
        = let hyp2 : (z : State) @$\rightarrow$@ Rel1 n s1 z @$\rightarrow$@
                     SemCond bInv z
              hyp2 = lem1 n
              s20 : State
              s20 = proj@$\text{1}$@ h
              t21 : Rel1 n s1 s20
              t21 = proj@$\text{1}$@ (proj@$\text{2}$@ h)
              t22 : (SemCond b s20) @$\times$@ (SemComm cm' s20 ss2)
              t22 = proj@$\text{2}$@ (RelOpState.deltaRestPre
                            (SemCond b) (SemComm cm') s20 ss2)
                    (proj@$\text{2}$@ (proj@$\text{2}$@ h))
              t23 : SemCond (bInv /\ b) s20
              t23 = proj@$\text{2}$@ (respAnd bInv b s20)
                    (hyp2 s20 t21 , proj@$\text{1}$@ t22)
          in hyp s20 ss2 t23 (proj@$\text{2}$@ t22)
      t20 : SemCond bInv s2 @$\times$@ SemCond (neg b) s2
      t20 = lem1 n s2 t16 , proj@$\text{2}$@ (respNeg b s2) t17