\begin{code}
{-# OPTIONS --safe --experimental-lossy-unification #-}

open import Prelude
open import Signatures
open import FinitenessConditions
open import FreeMonad.PackagedTheory

module Hoare.Calculus {β„“} (𝒯 : FullTheory β„“) where

open import FreeMonad.Quotiented 𝒯
open import Hoare.Definition 𝒯
open import Hoare.Lemmas 𝒯
open import Truth

⟨return_⟩ : Ξ© a β†’ Assertion a
⟨return x ⟩ .fst = return x
⟨return x ⟩ .snd .fst k = refl
⟨return x ⟩ .snd .snd k = refl

pass : βˆ€ {a} β†’ Term (Poly-⊀ {a})
pass = return Poly-tt

_<<_ : Term A β†’ Term B β†’ Term A
xs << ys = do x ← xs; ys; return x

sef :      (Ξ¦ : Assertion a) β†’ let Ο• = Ξ¦ .fst in
           (q : Term A) 

    β†’                  SEF 0 q
    β†’     --------------------------------
                   βŸ… Ο• βŸ† q >> pass βŸ… Ο• βŸ†

sef (Ο• , sefβŸ¨Ο•βŸ© , dsefβŸ¨Ο•βŸ©) q sef⟨q⟩ .proof k =

  (do a ← Ο•
      q >> return Poly-tt
      b ← Ο•
      k Poly-tt (a |β†’| b)) β‰‘βŸ¨ a ⇐ Ο• ΝΎ/ cong (_>> _) (sef⟨q⟩ _) ⟩

  (do a ← Ο•
      b ← Ο•
      k Poly-tt (a |β†’| b)) β‰‘βŸ¨ dsefβŸ¨Ο•βŸ© (Ξ» a b β†’ k Poly-tt (a |β†’| b)) ⟩

  (do a ← Ο•
      b ← Ο•
      k Poly-tt (a |β†’| a)) β‰‘βŸ¨ a ⇐ Ο• ΝΎ/ b ⇐ Ο• ΝΎ/ cong (k Poly-tt) (|β†’|-id a) ⟩

  (do a ← Ο•
      b ← Ο•
      k Poly-tt True) β‰‘Λ˜βŸ¨ a ⇐ Ο• ΝΎ/ cong (_>> _) (sef⟨q⟩ _) ⟩

  (do a ← Ο•
      x ← q >> return Poly-tt
      b ← Ο•
      k Poly-tt True) ∎

stateless : (Ο• : Ξ© a) (p : Term B) β†’ βŸ… return Ο• βŸ† [ p /⟨⟩] βŸ… return Ο• βŸ†
stateless Ο• p .proof k = cong ([ p /⟨⟩] >>_) (cong (k tt) (|β†’|-id Ο•))

dsef : {A : Type a}   β†’              (p : Term A)

                      β†’                  DET (β„“suc a) p
                      β†’ -------------------------------------------------
                          βŸ… return (True {a}) βŸ† x ← p βŸ… (do y ← p ; return (x |≑| y)) βŸ†

dsef {a = aβ„“} p dsef⟨p⟩ .proof k =

    (do a ← return (True {aβ„“})
        x ← p
        b ← (do y ← p ; return (x |≑| y))
        k x (a |β†’| b)) β‰‘βŸ¨βŸ©

    (do x ← p
        b ← (do y ← p ; return (x |≑| y))
        k x (True {aβ„“} |β†’| b)) β‰‘βŸ¨ x ⇐ p ΝΎ/ assoc p _ _ ⟩

    (do x ← p
        y ← p
        b ← return (x |≑| y)
        k x (True {aβ„“} |β†’| b)) β‰‘βŸ¨βŸ©

    (do x ← p
        y ← p
        k x (True {aβ„“} |β†’| (x |≑| y)))

          β‰‘βŸ¨ x ⇐ p ΝΎ/ y ⇐ p ΝΎ/ cong (k x) (|β†’|-idΛ‘ (x |≑| y)) ⟩

    (do x ← p
        y ← p
        k x (x |≑| y)) β‰‘βŸ¨ dsef⟨p⟩ _ ⟩

    (do x ← p
        y ← p
        k x (x |≑| x))

          β‰‘βŸ¨ x ⇐ p ΝΎ/ y ⇐ p ΝΎ/ cong (k x) (proves ∣ refl ∣) ⟩

    (do x ← p
        y ← p
        k x (True {aβ„“})) β‰‘Λ˜βŸ¨ dsef⟨p⟩ _ ⟩

    (do x ← p
        y ← p
        k x (True {aβ„“})) β‰‘βŸ¨βŸ©

    (do a ← return (True {aβ„“})
        x ← p
        y ← p
        k x (True {aβ„“})) β‰‘Λ˜βŸ¨ x ⇐ p ΝΎ/ assoc p _ _ ⟩

    (do a ← return (True {aβ„“})
        x ← p
        b ← (do y ← p ; return (x |≑| y))
        k x (True {aβ„“})) ∎

⟨&&&⟩ˑ :
  (Ο• : Term (Ξ© b))
  (ψ : A β†’ Term (Ξ© b))
  (Ο‡ : Ξ© b)
  (t : Term A) β†’
  βŸ… Ο• βŸ† x ← t βŸ… ψ x βŸ† β†’
  βŸ… return Ο‡ ⟨∧⟩ Ο• βŸ† x ← t βŸ… return Ο‡ ⟨∧⟩ ψ x βŸ†
⟨&&&⟩ˑ Ο• ψ Ο‡ t h .proof k =

  (do a ← return Ο‡ ⟨∧⟩ Ο•
      x ← t
      b ← return Ο‡ ⟨∧⟩ ψ x
      k x (a |β†’| b)) β‰‘βŸ¨ βŸͺassoc⟫ (return Ο‡) Ο• _|∧|_ _ ⟩

  (do a ← Ο•
      x ← t
      b ← return Ο‡ ⟨∧⟩ ψ x
      k x ((Ο‡ |∧| a) |β†’| b)) β‰‘βŸ¨ (a ⇐ Ο• ΝΎ/ x ⇐ t ΝΎ/ βŸͺassoc⟫ (return Ο‡) (ψ x) _|∧|_ _) ⟩

  (do a ← Ο•
      x ← t
      b ← ψ x
      k x ((Ο‡ |∧| a) |β†’| (Ο‡ |∧| b))) β‰‘βŸ¨ a ⇐ Ο• ΝΎ/ x ⇐ t ΝΎ/ b ⇐ ψ x ΝΎ/ cong (k x) ((Ξ» f x a β†’ snd (f (x , a))) iff Ξ» { f (x , a) β†’ x , f x a }) ⟩

  (do a ← Ο•
      x ← t
      b ← ψ x
      k x (Ο‡ |β†’| (a |β†’| b))) β‰‘βŸ¨ h .proof (Ξ» x r β†’ k x (Ο‡ |β†’| r)) ⟩

  (do a ← Ο•
      x ← t
      b ← ψ x
      k x (Ο‡ |β†’| True)) β‰‘βŸ¨ a ⇐ Ο• ΝΎ/ x ⇐ t ΝΎ/ b ⇐ ψ x ΝΎ/ cong (k x) (|β†’|-annΚ³ Ο‡) ⟩

  (do a ← Ο•
      x ← t
      b ← ψ x
      k x True) β‰‘Λ˜βŸ¨ a ⇐ Ο• ΝΎ/ x ⇐ t ΝΎ/ βŸͺassoc⟫ (return Ο‡) (ψ x) _|∧|_ _ ⟩

  (do a ← Ο•
      x ← t
      b ← return Ο‡ ⟨∧⟩ ψ x
      k x True) β‰‘Λ˜βŸ¨ βŸͺassoc⟫ (return Ο‡) Ο• _|∧|_ _ ⟩

  (do a ← return Ο‡ ⟨∧⟩ Ο•
      x ← t
      b ← return Ο‡ ⟨∧⟩ ψ x
      k x True) ∎

_ΝΎ,_ : Term A β†’ (A β†’ Term B) β†’ Term (A Γ— B)
xs ΝΎ, ys = do
  x ← xs
  y ← ys x
  return (x , y)

ΝΎ,-assoc : (xs : Term A) (ys : A β†’ Term B) (k : A β†’ B β†’ Term C) β†’
           (xs ΝΎ, ys) >>= uncurry k ≑ (do x ← xs ; y ← ys x ; k x y)
ΝΎ,-assoc xs ys k = assoc xs (Ξ» x β†’ ys x >>= Ξ» y β†’ return (x , y)) (uncurry k) ΝΎ x ⇐ xs ΝΎ/ assoc (ys x) _ _

seq : {A B : Type a}

    β†’                (Ξ¦ : Assertion a)         β†’ let Ο• = Ξ¦ .fst in
                     (Ξ¨ : A β†’ Assertion a)     β†’ let ψ = fst ∘ Ξ¨ in
                     (Ξ§ : A Γ— B β†’ Assertion a) β†’ let Ο‡ = fst ∘ Ξ§ in
                            {p : Term A}    {q : A β†’ Term B}

    β†’                               βŸ… Ο• βŸ† x ← p βŸ… ψ x βŸ†
    β†’                      (βˆ€ x β†’ βŸ… ψ x βŸ† y ← q x βŸ… Ο‡ (x , y) βŸ†)
    β†’              ------------------------------------------------
                             βŸ… Ο• βŸ† xy ← p ΝΎ, q βŸ… Ο‡ xy βŸ†

seq {a = aβ„“} (Ο• , sefβŸ¨Ο•βŸ© , dsefβŸ¨Ο•βŸ©) Ξ¨ Ξ§ {p = p} {q = q} lhs rhs .proof k =

  let Ο‡ = fst ∘ Ξ§
      ψ = fst ∘ Ψ
  in

  (do a ← Ο•
      (x , y) ← p ΝΎ, q
      b ← Ο‡ (x , y)
      k (x , y) (a |β†’| b))

        β‰‘βŸ¨ a ⇐ Ο• ΝΎ/ ΝΎ,-assoc p q _ ⟩

  (do a ← Ο•
      x ← p
      y ← q x
      b ← Ο‡ (x , y)
      k (x , y) (a |β†’| b))

        β‰‘Λ˜βŸ¨ a ⇐ Ο• ΝΎ/ x ⇐ p ΝΎ/ Ξ¨ x .snd .fst _ ⟩

  (do a ← Ο•
      x ← p
      i ← ψ x
      y ← q x
      b ← Ο‡ (x , y)
      k (x , y) (a |β†’| b))

        β‰‘Λ˜βŸ¨ a ⇐ Ο• ΝΎ/ x ⇐ p ΝΎ/ i ⇐ ψ x ΝΎ/ y ⇐ q x ΝΎ/ b ⇐ Ο‡ (x , y) ΝΎ/ cong (k (x , y)) (|β†’|-idΛ‘ _) ⟩

  (do a ← Ο•
      x ← p
      i ← ψ x
      y ← q x
      b ← Ο‡ (x , y)
      k (x , y) (True {aβ„“} |β†’| (a |β†’| b)))

        β‰‘Λ˜βŸ¨ a ⇐ Ο• ΝΎ/ x ⇐ p ΝΎ/ i ⇐ ψ x ΝΎ/ y ⇐ q x ΝΎ/ sef-dsef-cont (Ξ§ (x , y)) _ ⟩

  (do a ← Ο•
      x ← p
      i ← ψ x
      y ← q x
      b₁ ← Ο‡ (x , y)
      bβ‚‚ ← Ο‡ (x , y)
      k (x , y) (True {aβ„“} |β†’| (a |β†’| bβ‚‚)))

        β‰‘Λ˜βŸ¨ a ⇐ Ο• ΝΎ/ x ⇐ p ΝΎ/ rhs x .proof (Ξ» y r β†’ do bβ‚‚ ← Ο‡ (x , y) ; k (x , y) (r |β†’| a |β†’| bβ‚‚) ) ⟩

  (do a ← Ο•
      x ← p
      i ← ψ x
      y ← q x
      b₁ ← Ο‡ (x , y)
      bβ‚‚ ← Ο‡ (x , y)
      k (x , y) ((i |β†’| b₁) |β†’| (a |β†’| bβ‚‚)))

        β‰‘βŸ¨ a ⇐ Ο• ΝΎ/ x ⇐ p ΝΎ/ i ⇐ ψ x ΝΎ/ y ⇐ q x ΝΎ/ sef-dsef-cont (Ξ§ (x , y)) _ ⟩

  (do a ← Ο•
      x ← p
      i ← ψ x
      y ← q x
      b ← Ο‡ (x , y)
      k (x , y) ((i |β†’| b) |β†’| (a |β†’| b)))

        β‰‘Λ˜βŸ¨ a ⇐ Ο• ΝΎ/ x ⇐ p ΝΎ/ i ⇐ ψ x ΝΎ/ y ⇐ q x ΝΎ/ b ⇐ Ο‡ (x , y) ΝΎ/ cong (k (x , y)) (|β†’|-idΛ‘ _) ⟩

  (do a ← Ο•
      x ← p
      i ← ψ x
      y ← q x
      b ← Ο‡ (x , y)
      k (x , y) (True {aβ„“} |β†’| (i |β†’| b) |β†’| (a |β†’| b)))

        β‰‘Λ˜βŸ¨ sef-dsef-cont (Ο• , sefβŸ¨Ο•βŸ© , dsefβŸ¨Ο•βŸ©) _ ⟩

  (do a₁ ← Ο•
      aβ‚‚ ← Ο•
      x ← p
      i ← ψ x
      y ← q x
      b ← Ο‡ (x , y)
      k (x , y) (True {aβ„“} |β†’| (i |β†’| b) |β†’| (a₁ |β†’| b)))

        β‰‘Λ˜βŸ¨ a₁ ⇐ Ο• ΝΎ/ aβ‚‚ ⇐ Ο• ΝΎ/ x ⇐ p ΝΎ/ sef-dsef-cont (Ξ¨ x) _ ⟩

  (do a₁ ← Ο•
      aβ‚‚ ← Ο•
      x ← p
      i₁ ← ψ x
      iβ‚‚ ← ψ x
      y ← q x
      b ← Ο‡ (x , y)
      k (x , y) (True {aβ„“} |β†’| (iβ‚‚ |β†’| b) |β†’| (a₁ |β†’| b)))

        β‰‘Λ˜βŸ¨ a₁ ⇐ Ο• ΝΎ/ proof lhs (Ξ» x r β†’ do iβ‚‚ ← ψ x ; y ← q x ; b ← Ο‡ (x , y) ; k (x , y) (r |β†’| (iβ‚‚ |β†’| b) |β†’| (a₁ |β†’| b))) ⟩

  (do a₁ ← Ο•
      aβ‚‚ ← Ο•
      x ← p
      i₁ ← ψ x
      iβ‚‚ ← ψ x
      y ← q x
      b ← Ο‡ (x , y)
      k (x , y) ((aβ‚‚ |β†’| i₁) |β†’| (iβ‚‚ |β†’| b) |β†’| (a₁ |β†’| b)))

        β‰‘βŸ¨ sef-dsef-cont (Ο• , sefβŸ¨Ο•βŸ© , dsefβŸ¨Ο•βŸ©) _ ⟩

  (do a ← Ο•
      x ← p
      i₁ ← ψ x
      iβ‚‚ ← ψ x
      y ← q x
      b ← Ο‡ (x , y)
      k (x , y) ((a |β†’| i₁) |β†’| (iβ‚‚ |β†’| b) |β†’| (a |β†’| b)))

        β‰‘βŸ¨ a ⇐ Ο• ΝΎ/ x ⇐ p ΝΎ/ sef-dsef-cont (Ξ¨ x) _ ⟩

  (do a ← Ο•
      x ← p
      i ← ψ x
      y ← q x
      b ← Ο‡ (x , y)
      k (x , y) ((a |β†’| i) |β†’| (i |β†’| b) |β†’| (a |β†’| b)))

        β‰‘Λ˜βŸ¨ a ⇐ Ο• ΝΎ/ x ⇐ p ΝΎ/ i ⇐ ψ x ΝΎ/ y ⇐ q x ΝΎ/ b ⇐ Ο‡ (x , y) ΝΎ/ cong (k (x , y)) (|β†’|-curry _ _ _) ⟩

  (do a ← Ο•
      x ← p
      i ← ψ x
      y ← q x
      b ← Ο‡ (x , y)
      k (x , y) ((a |β†’| i) |∧| (i |β†’| b) |β†’| (a |β†’| b)))

        β‰‘βŸ¨ a ⇐ Ο• ΝΎ/ x ⇐ p ΝΎ/ i ⇐ ψ x ΝΎ/ y ⇐ q x ΝΎ/ b ⇐ Ο‡ (x , y) ΝΎ/ cong (k (x , y)) (|β†’|-trans a i b) ⟩

  (do a ← Ο•
      x ← p
      i ← ψ x
      y ← q x
      b ← Ο‡ (x , y)
      k (x , y) (True {aβ„“}))

        β‰‘βŸ¨ a ⇐ Ο• ΝΎ/ x ⇐ p ΝΎ/ Ξ¨ x .snd .fst _ ⟩

  (do a ← Ο•
      x ← p
      y ← q x
      b ← Ο‡ (x , y)
      k (x , y) True)

        β‰‘Λ˜βŸ¨ a ⇐ Ο• ΝΎ/ ΝΎ,-assoc p q _ ⟩

  (do a ← Ο•
      (x , y) ← p ΝΎ, q
      b ← Ο‡ (x , y)
      k (x , y) True) ∎



focus : {A B : Type a} {Ο• : Term (Ξ© b)} {ψ : B β†’ Term (Ξ© c)} {p : Term A}
      β†’ (sub : A β†’ B)
      β†’ βŸ… Ο• βŸ† x ← p βŸ… ψ (sub x) βŸ†
      β†’ βŸ… Ο• βŸ† x ← sub <$> p βŸ… ψ x βŸ†
focus {Ο• = Ο•} {ψ = ψ} {p = p} sub hr .proof k =
  (do a ← Ο•
      x ← sub <$> p
      b ← ψ x
      k x (a |β†’| b)) β‰‘βŸ¨ a ⇐ Ο• ΝΎ/ assoc p _ _ ⟩

  (do a ← Ο•
      x ← p
      b ← ψ (sub x)
      k (sub x) (a |β†’| b)) β‰‘βŸ¨ hr .proof (k ∘ sub) ⟩

  (do a ← Ο•
      x ← p
      b ← ψ (sub x)
      k (sub x) True) β‰‘Λ˜βŸ¨ a ⇐ Ο• ΝΎ/ assoc p _ _ ⟩

  (do a ← Ο•
      x ← sub <$> p
      b ← ψ x
      k x True) ∎

β‰‘βŸ…β‰‘βŸ†β‰‘ : {Ο• Ο•β€² : Term (Ξ© a)} {t tβ€² : Term A} {ψ Οˆβ€² : A β†’ Term (Ξ© b)} β†’ Ο• ≑ Ο•β€² β†’ t ≑ tβ€² β†’ (βˆ€ x β†’ ψ x ≑ Οˆβ€² x) β†’ βŸ… Ο• βŸ† x ← t βŸ… ψ x βŸ† β†’ βŸ… Ο•β€² βŸ† x ← tβ€² βŸ… Οˆβ€² x βŸ†
β‰‘βŸ…β‰‘βŸ†β‰‘ p q r = subst (Hoare _ _) (funExt r) ∘ substβ‚‚ (Ξ» x y β†’ Hoare x y _) p q

subst-βŸ…βŸ† : {Ο• : Term (Ξ© b)} {p : Term A} {ψ : A β†’ Term (Ξ© c)} {q : Term A}
        β†’ p ≑ q
        β†’ βŸ… Ο• βŸ† x ← p βŸ… ψ x βŸ†
        β†’ βŸ… Ο• βŸ† x ← q βŸ… ψ x βŸ†
subst-βŸ…βŸ† {Ο• = Ο•} {ψ = ψ} = subst (flip (Hoare Ο•) ψ)

seqβ€² : {A B : Type a}
    β†’                (Ξ¦ : Assertion a)     β†’ let Ο• = Ξ¦ .fst in
                     (Ξ¨ : A β†’ Assertion a) β†’ let ψ = fst ∘ Ξ¨ in
                     (Ξ§ : B β†’ Assertion a) β†’ let Ο‡ = fst ∘ Ξ§ in
                            {p : Term A}    {q : A β†’ Term B}

    β†’                               βŸ… Ο• βŸ† x ← p βŸ… ψ x βŸ†
    β†’                      (βˆ€ x β†’ βŸ… ψ x βŸ† y ← q x βŸ… Ο‡ y βŸ†)
    β†’              ------------------------------------------------
                             βŸ… Ο• βŸ† y ← p >>= q βŸ… Ο‡ y βŸ†
seqβ€² Ξ¦ Ξ¨ Ξ§ {p = p} {q = q} lhs rhs =
  let h  = seq Φ Ψ (Χ ∘ snd) lhs rhs
      hβ€² = focus snd h
  in subst-βŸ…βŸ† (snd <$> (p ΝΎ, q) β‰‘βŸ¨ assoc p  _ _ ΝΎ x ⇐ p ΝΎ/ assoc (q x) _ _ ΝΎ >>=-idΚ³ (q x) ⟩ (p >>= q) ∎) hβ€²

seq⁻ : {A B : Type a}
    β†’                (Ξ¦ : Assertion a)     β†’ let Ο• = Ξ¦ .fst in
                     (Ξ¨ : A β†’ Assertion a) β†’ let ψ = fst ∘ Ξ¨ in
                     (Ξ§ : B β†’ Assertion a) β†’ let Ο‡ = fst ∘ Ξ§ in
                            {p : Term A}    {q : A β†’ Term B}

    β†’                      (βˆ€ x β†’ βŸ… ψ x βŸ† y ← q x βŸ… Ο‡ y βŸ†)
    β†’                               βŸ… Ο• βŸ† x ← p βŸ… ψ x βŸ†
    β†’              ------------------------------------------------
                             βŸ… Ο• βŸ† y ← p >>= q βŸ… Ο‡ y βŸ†
seq⁻ Ξ¦ Ξ¨ Ξ§ = flip (seqβ€² Ξ¦ Ξ¨ Ξ§)

seq-<< : {A B : Type a}
    β†’                (Ξ¦ : Assertion a)     β†’ let Ο• = Ξ¦ .fst in
                     (Ξ¨ : A β†’ Assertion a) β†’ let ψ = fst ∘ Ξ¨ in
                     (Ξ§ : A β†’ Assertion a) β†’ let Ο‡ = fst ∘ Ξ§ in
                            {p : Term A}    {q : Term B}

    β†’                               βŸ… Ο• βŸ† x ← p βŸ… ψ x βŸ†
    β†’                      (βˆ€ x β†’ βŸ… ψ x βŸ† y ← q βŸ… Ο‡ x βŸ†)
    β†’              ------------------------------------------------
                             βŸ… Ο• βŸ† y ← p << q βŸ… Ο‡ y βŸ†
seq-<< Ξ¦ Ξ¨ Ξ§ {p = p} {q = q} lhs rhs =
  let h = seq Φ Ψ (Χ ∘ fst) lhs rhs
      hβ€² = focus fst h
  in subst-βŸ…βŸ† (assoc p _ _ ΝΎ x ⇐ p ΝΎ/ assoc q _ _) hβ€²


module _
  {A : Type a}
  (Ο• : Assertion a)
  (p : Term A)
  (ψ Ο‡ : A β†’ Assertion a)
  where
    imply : (βˆ€ x β†’ βŸ… ψ x .fst βŸ† pass βŸ… Ο‡ x .fst βŸ†)
          β†’ βŸ… Ο• .fst βŸ† x ← p βŸ… ψ x .fst βŸ†
          β†’ βŸ… Ο• .fst βŸ† x ← p βŸ… Ο‡ x .fst βŸ†
    imply imp h = subst-βŸ…βŸ† (>>=-idΚ³ p) ( seqβ€² Ο• ψ Ο‡ h Ξ» x β†’ focus (const x) (imp x))

βŸ…sndβŸ† : {A : Type a} (Ξ¦ : Assertion a) (p : Term A)
        (Οˆβ‚ : A β†’ Term (Ξ© a)) β†’
        (sefβŸ¨Οˆβ‚βŸ© : βˆ€ x β†’ SEF (β„“suc a) (Οˆβ‚ x))
        (Ξ¨β‚‚ : A β†’ Assertion a) β†’
      βŸ… Ξ¦ .fst βŸ† x ← p βŸ… Οˆβ‚ x ⟨∧⟩ Ξ¨β‚‚ x .fst βŸ† β†’ βŸ… Ξ¦ .fst βŸ† x ← p βŸ… Ξ¨β‚‚ x .fst βŸ†
βŸ…sndβŸ† Ξ¦ p Οˆβ‚ sefβŸ¨Οˆβ‚βŸ© Ξ¨β‚‚ prf .proof k =
  let Ο• = Ξ¦ .fst
      Οˆβ‚‚ = fst ∘ Ξ¨β‚‚
  in

  (do a ← Ο•
      x ← p
      bβ‚‚ ← Οˆβ‚‚ x
      k x (a |β†’| bβ‚‚)) β‰‘Λ˜βŸ¨ a ⇐ Ο• ΝΎ/ Ξ¦ .snd .fst _ ⟩

  (do a ← Ο•
      aβ€² ← Ο•
      x ← p
      bβ‚‚ ← Οˆβ‚‚ x
      k x (a |β†’| bβ‚‚)) β‰‘Λ˜βŸ¨ a ⇐ Ο• ΝΎ/ aβ€² ⇐ Ο• ΝΎ/ x ⇐ p ΝΎ/ sefβŸ¨Οˆβ‚βŸ© x _ ⟩

  (do a ← Ο•
      aβ€² ← Ο•
      x ← p
      b₁′ ← Οˆβ‚ x
      bβ‚‚ ← Οˆβ‚‚ x
      k x (a |β†’| bβ‚‚)) β‰‘Λ˜βŸ¨ a ⇐ Ο• ΝΎ/ aβ€² ⇐ Ο• ΝΎ/ x ⇐ p ΝΎ/ b₁′ ⇐ Οˆβ‚ x ΝΎ/ Ξ¨β‚‚ x .snd .fst _ ⟩

  (do a ← Ο•
      aβ€² ← Ο•
      x ← p
      b₁′ ← Οˆβ‚ x
      bβ‚‚β€² ← Οˆβ‚‚ x
      bβ‚‚ ← Οˆβ‚‚ x
      k x (a |β†’| bβ‚‚)) β‰‘Λ˜βŸ¨ a ⇐ Ο• ΝΎ/ aβ€² ⇐ Ο• ΝΎ/ x ⇐ p ΝΎ/ βŸͺassoc⟫ (Οˆβ‚ x) (Οˆβ‚‚ x) _|∧|_ _ ⟩

  (do a ← Ο•
      aβ€² ← Ο•
      x ← p
      bβ€² ← Οˆβ‚ x ⟨∧⟩ Οˆβ‚‚ x
      bβ‚‚ ← Οˆβ‚‚ x
      k x (a |β†’| bβ‚‚)) β‰‘βŸ¨ a ⇐ Ο• ΝΎ/ aβ€² ⇐ Ο• ΝΎ/ x ⇐ p ΝΎ/ bβ€² ⇐ Οˆβ‚ x ⟨∧⟩ Οˆβ‚‚ x ΝΎ/ bβ‚‚ ⇐ Οˆβ‚‚ x ΝΎ/ cong (k x) (cong (a |β†’|_) ((_, _) iff fst)) ⟩

  (do a ← Ο•
      aβ€² ← Ο•
      x ← p
      bβ€² ← Οˆβ‚ x ⟨∧⟩ Οˆβ‚‚ x
      bβ‚‚ ← Οˆβ‚‚ x
      k x (a |β†’| (bβ‚‚ |∧| True))) β‰‘Λ˜βŸ¨ a ⇐ Ο• ΝΎ/  prf .proof (Ξ» x t β†’ do bβ‚‚ ← Οˆβ‚‚ x; k x (a |β†’| (bβ‚‚ |∧| t))) ⟩

  (do a ← Ο•
      aβ€² ← Ο•
      x ← p
      bβ€² ← Οˆβ‚ x ⟨∧⟩ Οˆβ‚‚ x
      bβ‚‚ ← Οˆβ‚‚ x
      k x (a |β†’| (bβ‚‚ |∧| (aβ€² |β†’| bβ€²)))) β‰‘βŸ¨ sef-dsef-cont Ξ¦ _ ⟩

  (do a ← Ο•
      x ← p
      bβ€² ← Οˆβ‚ x ⟨∧⟩ Οˆβ‚‚ x
      bβ‚‚ ← Οˆβ‚‚ x
      k x (a |β†’| (bβ‚‚ |∧| (a |β†’| bβ€²)))) β‰‘βŸ¨ (a ⇐ Ο• ΝΎ/ x ⇐ p ΝΎ/ βŸͺassoc⟫ (Οˆβ‚ x) (Οˆβ‚‚ x) _|∧|_ _ ) ⟩

  (do a ← Ο•
      x ← p
      b₁ ← Οˆβ‚ x
      bβ‚‚β€² ← Οˆβ‚‚ x
      bβ‚‚ ← Οˆβ‚‚ x
      k x (a |β†’| (bβ‚‚ |∧| (a |β†’| (b₁ |∧| bβ‚‚β€²))))) β‰‘βŸ¨ a ⇐ Ο• ΝΎ/ x ⇐ p ΝΎ/ b₁ ⇐ Οˆβ‚ x ΝΎ/ sef-dsef-cont (Ξ¨β‚‚ x) _ ⟩

  (do a ← Ο•
      x ← p
      b₁ ← Οˆβ‚ x
      bβ‚‚ ← Οˆβ‚‚ x
      k x (a |β†’| (bβ‚‚ |∧| (a |β†’| (b₁ |∧| bβ‚‚))))) β‰‘βŸ¨ a ⇐ Ο• ΝΎ/ x ⇐ p ΝΎ/ b₁ ⇐ Οˆβ‚ x ΝΎ/ bβ‚‚ ⇐ Οˆβ‚‚ x ΝΎ/ cong (k x) ((Ξ» f x β†’ f x .snd x .fst , f x .fst) iff Ξ» f x β†’ f x .snd , const (f x)) ⟩

  (do a ← Ο•
      x ← p
      b₁ ← Οˆβ‚ x
      bβ‚‚ ← Οˆβ‚‚ x
      k x (a |β†’| (b₁ |∧| bβ‚‚))) β‰‘Λ˜βŸ¨ a ⇐ Ο• ΝΎ/ x ⇐ p ΝΎ/ βŸͺassoc⟫ (Οˆβ‚ x) (Οˆβ‚‚ x) _|∧|_ _ ⟩

  (do a ← Ο•
      x ← p
      bβ‚βˆ§bβ‚‚ ← Οˆβ‚ x ⟨∧⟩ Οˆβ‚‚ x
      k x (a |β†’| bβ‚βˆ§bβ‚‚)) β‰‘βŸ¨ prf .proof k ⟩

  (do a ← Ο•
      x ← p
      bβ‚βˆ§bβ‚‚ ← Οˆβ‚ x ⟨∧⟩ Οˆβ‚‚ x
      k x True) β‰‘βŸ¨ a ⇐ Ο• ΝΎ/ x ⇐ p ΝΎ/ βŸͺassoc⟫ (Οˆβ‚ x) (Οˆβ‚‚ x) _|∧|_ _ ⟩

  (do a ← Ο•
      x ← p
      b₁ ← Οˆβ‚ x
      bβ‚‚ ← Οˆβ‚‚ x
      k x True) β‰‘βŸ¨ a ⇐ Ο• ΝΎ/ x ⇐ p ΝΎ/  sefβŸ¨Οˆβ‚βŸ© x _ ⟩


  (do a ← Ο•
      x ← p
      bβ‚‚ ← Οˆβ‚‚ x
      k x True) ∎

βŸ…β†’βŸ†True : (Ο• : Term (Ξ© a)) (t : Term B) β†’ βŸ… Ο• βŸ† _ ← t βŸ… return (True {a = c}) βŸ†
βŸ…β†’βŸ†True Ο• t .proof k = a ⇐ Ο• ΝΎ/ x ⇐ t ΝΎ/ cong (k x) (|β†’|-annΚ³ _)


module _ {A : Type a} (Ξ¦ : Assertion a) {t : Term A} {ψ : A β†’ Term (Ξ© a)} (f : Ξ© a β†’ Ξ© a) where
  private Ο• = fst Ξ¦

  β†’βŸ…βˆ™βŸ† : (i : βˆ€ {x} β†’ ProofOf (f x) β†’ ProofOf x)
       β†’ βŸ… Ο• βŸ† x ← t βŸ… ψ x βŸ†
       β†’ βŸ… f <$> Ο• βŸ† x ← t βŸ… ψ x βŸ†
  β†’βŸ…βˆ™βŸ† i h .proof k =
    (do a ← f <$> Ο•
        x ← t
        b ← ψ x
        k x (a |β†’| b))

      β‰‘βŸ¨ assoc Ο• _ _ ⟩

    (do a ← Ο•
        x ← t
        b ← ψ x
        k x (f a |β†’| b))

      β‰‘βŸ¨ a ⇐ Ο• ΝΎ/ x ⇐ t ΝΎ/ b ⇐ ψ x ΝΎ/ cong (k x) ((Ξ» k x y β†’ k x) iff Ξ» k x β†’ k x (i x)) ⟩

    (do a ← Ο•
        x ← t
        b ← ψ x
        k x (f a |β†’| a |β†’| b))

      β‰‘Λ˜βŸ¨ sef-dsef-cont Ξ¦ _ ⟩

    (do a  ← Ο•
        aβ€² ← Ο•
        x ← t
        b ← ψ x
        k x (f a |β†’| aβ€² |β†’| b))

      β‰‘βŸ¨ a ⇐ Ο• ΝΎ/ h .proof (Ξ» x r β†’ k x (f a |β†’| r)) ⟩

    (do a  ← Ο•
        aβ€² ← Ο•
        x ← t
        b ← ψ x
        k x (f a |β†’| True))

      β‰‘βŸ¨ sef-dsef-cont Ξ¦ _ ⟩

    (do a ← Ο•
        x ← t
        b ← ψ x
        k x (f a |β†’| True))

      β‰‘βŸ¨ a ⇐ Ο• ΝΎ/ x ⇐ t ΝΎ/ b ⇐ ψ x ΝΎ/ cong (k x) (|β†’|-annΚ³ (f a)) ⟩

    (do a ← Ο•
        x ← t
        b ← ψ x
        k x True)

      β‰‘Λ˜βŸ¨ assoc Ο• _ _ ⟩

    (do a ← f <$> Ο•
        x ← t
        b ← ψ x
        k x True) ∎

module _ {A : Type a} (Ξ¦ : Assertion a) {t : Term A} (Ξ¨ : A β†’ Assertion a) (f : Ξ© a β†’ Ξ© a) where
  private
    ψ = fst ∘ Ψ
    Ο• = fst Ξ¦

  βŸ…βˆ™βŸ†β†’ : (i : βˆ€ {x} β†’ ProofOf x β†’ ProofOf (f x))
       β†’ βŸ… Ο• βŸ† x ← t βŸ… ψ x βŸ†
       β†’ βŸ… Ο• βŸ† x ← t βŸ… f <$> ψ x βŸ†
  βŸ…βˆ™βŸ†β†’ i h =
    subst-βŸ…βŸ† (>>=-idΚ³ _) (seqβ€² Ξ¦ Ξ¨ (Ξ» x β†’ _ ,  sef-<$> f (ψ x) (Ξ¨ x .snd .fst) , det-<$> f (ψ x) (Ξ¨ x .snd .snd)) h
      Ξ» where x .proof k β†’
                            (do a ← ψ x
                                b ← f <$> ψ x
                                k _ (a |β†’| b)) β‰‘βŸ¨ a ⇐ ψ x ΝΎ/ assoc (ψ x) _ _ ⟩

                            (do a ← ψ x
                                b ← ψ x
                                k _ (a |β†’| f b)) β‰‘βŸ¨ sef-dsef-cont (Ξ¨ x) _ ⟩

                            (do a ← ψ x
                                k _ (a |β†’| f a)) β‰‘βŸ¨ a ⇐ ψ x ΝΎ/ cong (k _) (proves i) ⟩

                            (do a ← ψ x
                                k _ True) β‰‘Λ˜βŸ¨ Ξ¨ x .snd .fst _ ⟩

                            (do a ← ψ x
                                b ← ψ x
                                k _ True) β‰‘Λ˜βŸ¨ a ⇐ ψ x ΝΎ/ assoc (ψ x) _ _ ⟩

                            (do a ← ψ x
                                b ← f <$> ψ x
                                k _ True) ∎
        )



FalseβŸ…β†’βŸ† : (t : Term A) (Ο• : A β†’ Term (Ξ© b)) β†’ βŸ… return (False {a = c}) βŸ† x ← t βŸ… Ο• x βŸ†
FalseβŸ…β†’βŸ† t Ο• .proof k = x ⇐ t ΝΎ/ b ⇐ Ο• x ΝΎ/ cong (k x) (|β†’|-annΛ‘ _)

βŸ…idβŸ† : (Ο• : Term (Ξ© a)) β†’ DET (β„“suc a) Ο• β†’ βŸ… Ο• βŸ† pass {a = a} βŸ… Ο• βŸ†
βŸ…idβŸ† Ο• det .proof k = det (Ξ» a b β†’ k Poly-tt (a |β†’| b)) ΝΎ a ⇐ Ο• ΝΎ/ b ⇐ Ο• ΝΎ/ cong (k Poly-tt) (|β†’|-id _)

βŸ…retβŸ† : (Ο• : Ξ© a) (t : Term B) β†’ βŸ… return Ο• βŸ† _ ← t βŸ… return Ο• βŸ†
βŸ…retβŸ† Ο• t .proof k = x ⇐ t ΝΎ/ cong (k x) (|β†’|-id Ο•)

β‰‘βŸ…βˆ™βŸ†β‰‘ : {Ο• Ο•β€² : Term (Ξ© a)} {t : Term A} {ψ Οˆβ€² : A β†’ Term (Ξ© b)} β†’ Ο• ≑ Ο•β€² β†’ (βˆ€ x β†’ ψ x ≑ Οˆβ€² x) β†’ βŸ… Ο• βŸ† x ← t βŸ… ψ x βŸ† β†’ βŸ… Ο•β€² βŸ† x ← t βŸ… Οˆβ€² x βŸ†
β‰‘βŸ…βˆ™βŸ†β‰‘ {t = t} p q = substβ‚‚ (Ξ» p q β†’ Hoare p t q) p (funExt q)

β‰‘βŸ…βˆ™βŸ† : {Ο• Ο•β€² : Term (Ξ© a)} {t : Term A} {ψ : A β†’ Term (Ξ© b)} β†’ Ο• ≑ Ο•β€² β†’ βŸ… Ο• βŸ† x ← t βŸ… ψ x βŸ† β†’ βŸ… Ο•β€² βŸ† x ← t βŸ… ψ x βŸ†
β‰‘βŸ…βˆ™βŸ† {t = t} {ψ = ψ} = subst (Ξ» p β†’ Hoare p t ψ)

βŸ…βˆ™βŸ†β‰‘ : {Ο• : Term (Ξ© a)} {t : Term A} {ψ Οˆβ€² : A β†’ Term (Ξ© b)} β†’ (βˆ€ x β†’ ψ x ≑ Οˆβ€² x) β†’ βŸ… Ο• βŸ† x ← t βŸ… ψ x βŸ† β†’ βŸ… Ο• βŸ† x ← t βŸ… Οˆβ€² x βŸ†
βŸ…βˆ™βŸ†β‰‘ {Ο• = Ο•} {t = t} e = subst (Ξ» p β†’ Hoare Ο• t p) (funExt e)

⟨&&&⟩ʳ :
  (Ο• : Term (Ξ© b))
  (ψ : A β†’ Term (Ξ© b))
  (Ο‡ : Ξ© b)
  (t : Term A) β†’
  βŸ… Ο• βŸ† x ← t βŸ… ψ x βŸ† β†’
  βŸ… Ο• ⟨∧⟩ return Ο‡ βŸ† x ← t βŸ… ψ x ⟨∧⟩ return Ο‡ βŸ†
⟨&&&⟩ʳ Ο• ψ Ο‡ t h = β‰‘βŸ…βˆ™βŸ†β‰‘ (a ⇐ Ο• ΝΎ/ cong return (∧-com Ο‡ a)) (Ξ» x β†’ b ⇐ ψ x ΝΎ/ cong return (∧-com Ο‡ b)) (⟨&&&⟩ˑ Ο• ψ Ο‡ t h)

False⟨∧⟩ : (Ο• : Term (Ξ© a)) β†’ SEF (β„“suc a) Ο• β†’ return False ⟨∧⟩ Ο• ≑ return False
False⟨∧⟩ Ο• sef =
  return False ⟨∧⟩ Ο• β‰‘βŸ¨βŸ©
  (do f ← return False; p ← Ο•; return (f |∧| p)) β‰‘βŸ¨βŸ©
  (do p ← Ο•; return (False |∧| p)) β‰‘βŸ¨ p ⇐ Ο• ΝΎ/ cong return (fst iff Ξ» ()) ⟩
  (do p ← Ο•; return False) β‰‘βŸ¨ sef (return False) ⟩
  return False ∎

True⟨∧⟩ : (Ο• : Term (Ξ© a)) β†’ return True ⟨∧⟩ Ο• ≑ Ο•
True⟨∧⟩ Ο• = (a ⇐ Ο• ΝΎ/ cong return (∧-id a)) ΝΎ <$>-id Ο•


weaken : {A : Type a}
       β†’ (Ξ¦ : Assertion a) β†’ let Ο• = Ξ¦ .fst in
         (Ξ¨ : A β†’ Assertion a) β†’ let ψ = fst ∘ Ξ¨ in
         {p : Term A}
       β†’ (Ξ§ : Assertion a) β†’ let Ο‡ = Ξ§ .fst in
         βŸ… Ο‡ βŸ† pass βŸ… Ο• βŸ†
       β†’ βŸ… Ο• βŸ† x ← p βŸ… ψ x βŸ†
       β†’ βŸ… Ο‡ βŸ† x ← p βŸ… ψ x βŸ†
weaken Ξ¦ Ξ¨ {p = p} Ξ§ lhs rhs =
  let h = seq Ξ§ (Ξ» _ β†’ Ξ¦) (Ξ» { (_ , x) β†’ Ξ¨ x }) lhs (Ξ» _ β†’ rhs)
      hβ€² = focus snd h
  in subst-βŸ…βŸ† (assoc (return Poly-tt) (Ξ» x β†’ p >>= Ξ» y β†’ return (x , y)) (return βˆ˜β€² snd) ΝΎ assoc p _ _ ΝΎ >>=-idΚ³ p) hβ€²

if : {A : Type a}
   β†’                    (Ο• : Term (Ξ© a)) (ψ : A β†’ Term (Ξ© a)) 
   β†’
   (p : Term A) (q : Term A) (b : Bool) β†’
   βŸ… return (|T|     b)  ⟨∧⟩ Ο• βŸ† x ← p βŸ… ψ x βŸ† β†’
   βŸ… return (|T| (!  b)) ⟨∧⟩ Ο• βŸ† x ← q βŸ… ψ x βŸ† β†’    
   βŸ… Ο• βŸ† x ← if b then p else q βŸ… ψ x βŸ†

if Ο• ψ p q =
  bool 
    (Ξ» _ rhs β†’ subst (Ξ» e β†’ βŸ… e βŸ† x ← q βŸ… ψ x βŸ†) (∧-lemma Ο•) rhs)
    (Ξ» lhs _ β†’ subst (Ξ» e β†’ βŸ… e βŸ† x ← p βŸ… ψ x βŸ†) (∧-lemma Ο•) lhs)
    where
    ∧-lemma : (x : Term (Ξ© a)) β†’ (True |∧|_) <$> x ≑ x
    ∧-lemma x = cong (_<$> x) (funExt ∧-id) ; <$>-id x

conj : {A : Type a}
     β†’                 (Ξ¦ : Assertion a) β†’ let Ο• = fst Ξ¦ in
                       (ψ : A β†’ Term (Ξ© a)) β†’ (βˆ€ x β†’ SEF (β„“suc a) (ψ x))
     β†’                 (Ο‡ : A β†’ Term (Ξ© a)) 
     β†’                              (p : Term A)
     β†’
\end{code}
%<*conj>
\begin{code}
      (βŸ… Ο• βŸ† x ← p βŸ… ψ x βŸ†) β†’ (βŸ… Ο• βŸ† x ← p βŸ… Ο‡ x βŸ†) β†’ (βŸ… Ο• βŸ† x ← p βŸ… ψ x ⟨∧⟩ Ο‡ x βŸ†)
\end{code}
%</conj>
\begin{code}

conj {a = aβ„“} (Ο• , sefβŸ¨Ο•βŸ© , dsefβŸ¨Ο•βŸ©) ψ sef⟨ψ⟩ Ο‡ p lhs rhs .proof k =

  (do a ← Ο•
      x ← p
      b ← (ψ x ⟨∧⟩ Ο‡ x)
      k x (a |β†’| b)) β‰‘βŸ¨βŸ©

  (do a ← Ο•
      x ← p
      b ← (do b₁ ← ψ x ; bβ‚‚ ← Ο‡ x ; return (b₁ |∧| bβ‚‚))
      k x (a |β†’| b)) β‰‘βŸ¨ a ⇐ Ο• ΝΎ/ x ⇐ p ΝΎ/ assoc (ψ x) _ _ ΝΎ b₁ ⇐ ψ x ΝΎ/ assoc (Ο‡ x) _ _ ⟩

  (do a ← Ο•
      x ← p
      b₁ ← ψ x
      bβ‚‚ ← Ο‡ x
      k x (a |β†’| (b₁ |∧| bβ‚‚)))

        β‰‘βŸ¨ a ⇐ Ο• ΝΎ/ x ⇐ p ΝΎ/ b₁ ⇐ ψ x ΝΎ/ bβ‚‚ ⇐ Ο‡ x ΝΎ/ cong (k x) (|β†’|-|∧| a b₁ bβ‚‚) ⟩

  (do a ← Ο•
      x ← p
      b₁ ← ψ x
      bβ‚‚ ← Ο‡ x
      k x ((a |β†’| b₁) |∧| (a |β†’| bβ‚‚)))

      β‰‘Λ˜βŸ¨ sef-dsef-cont (Ο• , sefβŸ¨Ο•βŸ© , dsefβŸ¨Ο•βŸ©) _ ⟩

  (do a₁ ← Ο•
      aβ‚‚ ← Ο•
      x ← p
      b₁ ← ψ x
      bβ‚‚ ← Ο‡ x
      k x ((aβ‚‚ |β†’| b₁) |∧| (a₁ |β†’| bβ‚‚)))

      β‰‘βŸ¨ a₁ ⇐ Ο• ΝΎ/ lhs .proof (Ξ» x r β†’ do bβ‚‚ ← Ο‡ x ; k x (r |∧| (a₁ |β†’| bβ‚‚))) ⟩

  (do a₁ ← Ο•
      aβ‚‚ ← Ο•
      x ← p
      ψ x
      bβ‚‚ ← Ο‡ x
      k x (True {aβ„“} |∧| (a₁ |β†’| bβ‚‚))) β‰‘βŸ¨ sef-dsef-cont (Ο• , sefβŸ¨Ο•βŸ© , dsefβŸ¨Ο•βŸ©) _ ⟩

  (do a ← Ο•
      x ← p
      ψ x
      bβ‚‚ ← Ο‡ x
      k x (True {aβ„“} |∧| (a |β†’| bβ‚‚)))

        β‰‘βŸ¨ a ⇐ Ο• ΝΎ/ x ⇐ p ΝΎ/ _ ⇐ ψ x ΝΎ/ bβ‚‚ ⇐ Ο‡ x ΝΎ/ cong (k x) (∧-id _) ⟩

  (do a ← Ο•
      x ← p
      ψ x
      bβ‚‚ ← Ο‡ x
      k x (a |β†’| bβ‚‚)) β‰‘βŸ¨ a ⇐ Ο• ΝΎ/ x ⇐ p ΝΎ/ sef⟨ψ⟩ x _ ⟩

  (do a ← Ο•
      x ← p
      bβ‚‚ ← Ο‡ x
      k x (a |β†’| bβ‚‚)) β‰‘βŸ¨ rhs .proof k ⟩

  (do a ← Ο•
      x ← p
      Ο‡ x
      k x True) β‰‘Λ˜βŸ¨ a ⇐ Ο• ΝΎ/ x ⇐ p ΝΎ/ sef⟨ψ⟩ x _ ⟩

  (do a ← Ο•
      x ← p
      ψ x
      Ο‡ x
      k x True) β‰‘Λ˜βŸ¨ a ⇐ Ο• ΝΎ/ x ⇐ p ΝΎ/ assoc (ψ x) _ _ ΝΎ b ⇐ ψ x ΝΎ/ assoc (Ο‡ x) _ _ ⟩

  (do a ← Ο•
      x ← p
      ψ x ⟨∧⟩ Ο‡ x
      k x True) ∎

βŸ…βˆ§βŸ† : {A : Type a} {p : Ξ© a} (Ο• : Assertion a) {t : Term A} (ψ : A β†’ Assertion a)
   β†’ βŸ… Ο• .fst βŸ† x ← t βŸ… ψ x .fst βŸ† β†’ βŸ… return p ⟨∧⟩ Ο• .fst βŸ† x ← t βŸ… return p ⟨∧⟩ ψ x .fst βŸ†
βŸ…βˆ§βŸ† {p = p} Ο• {t = t} ψ rhs =
  conj
    (return p ⟨∧⟩ Ο• .fst , sef-<$> _ _ (Ο• .snd .fst) , det-<$> _ _ (Ο• .snd .snd))
    (Ξ» _ β†’ return p)
    ( Ξ» x k β†’ refl)
    (Ξ» x β†’ ψ x .fst)
    t
    (Ξ» where .proof k β†’ (do a ← return p ⟨∧⟩ Ο• .fst; x ← t; b ← return p; k x (a |β†’| b)) β‰‘βŸ¨ assoc (Ο• .fst) _ _ ⟩
                        (do a ← Ο• .fst; x ← t; b ← return p; k x ((p |∧| a) |β†’| b)) β‰‘βŸ¨βŸ©
                        (do a ← Ο• .fst; x ← t; k x ((p |∧| a) |β†’| p)) β‰‘βŸ¨ a ⇐ Ο• .fst ΝΎ/ x ⇐ t ΝΎ/ cong (k x) (proves fst) ⟩
                        (do a ← Ο• .fst; x ← t; k x True) β‰‘Λ˜βŸ¨ assoc (Ο• .fst) _ _ ⟩
                        (do a ← return p ⟨∧⟩ Ο• .fst; x ← t; b ← return p; k x True) ∎
    )
    (β†’βŸ…βˆ™βŸ† (_ , Ο• .snd .fst ,  Ο• .snd .snd) _ snd rhs)

module _ {A : Type a} where
\end{code}
\begin{code}
  disj :                    (Ο• : Term (Ξ© a))
       β†’                    (ψ : Term (Ξ© a)) β†’ SEF (β„“suc a) ψ
       β†’                    (Ξ§ : A β†’ Assertion a) β†’ let Ο‡ = fst ∘ Ξ§ in 
                            (p : Term A)
       β†’
       (βŸ… Ο• βŸ† x ← p βŸ… Ο‡ x βŸ†) β†’ (βŸ… ψ βŸ† x ← p βŸ… Ο‡ x βŸ†) β†’ (βŸ… Ο• ⟨∨⟩ ψ βŸ† x ← p βŸ… Ο‡ x βŸ†)
  disj Ο• ψ sef⟨ψ⟩ Ξ§ p lhs rhs .proof k = let Ο‡ = fst ∘ Ξ§ in
    (do a ← Ο• βŸͺ _|∨|_ ⟫ ψ
        x ← p
        b ← Ο‡ x
        k x (a |β†’| b)) β‰‘βŸ¨ βŸͺassoc⟫ Ο• ψ _|∨|_ _ ⟩
  
    (do a₁ ← Ο•
        aβ‚‚ ← ψ
        x ← p
        b ← Ο‡ x
        k x (a₁ |∨| aβ‚‚ |β†’| b))
  
          β‰‘βŸ¨ a₁ ⇐ Ο• ΝΎ/ aβ‚‚ ⇐ ψ ΝΎ/ x  ⇐ p ΝΎ/ b  ⇐ Ο‡ x ΝΎ/ cong (k x) (|∨|-|β†’| _ _ _) ⟩
  
    (do a₁ ← Ο•
        aβ‚‚ ← ψ
        x ← p
        b ← Ο‡ x
        k x ((a₁ |β†’| b) |∧| (aβ‚‚ |β†’| b))) β‰‘Λ˜βŸ¨ a₁ ⇐ Ο• ΝΎ/ aβ‚‚ ⇐ ψ ΝΎ/ x ⇐ p ΝΎ/ sef-dsef-cont (Ξ§ x) _ ⟩
  
    (do a₁ ← Ο•
        aβ‚‚ ← ψ
        x ← p
        b₁ ← Ο‡ x
        bβ‚‚ ← Ο‡ x
        k x ((a₁ |β†’| bβ‚‚) |∧| (aβ‚‚ |β†’| b₁))) β‰‘βŸ¨ a₁ ⇐ Ο• ΝΎ/ rhs .proof (Ξ» x r β†’ Ο‡ x >>= Ξ» bβ‚‚ β†’ k x ((a₁ |β†’| bβ‚‚) |∧| r)) ⟩
  
    (do a₁ ← Ο•
        aβ‚‚ ← ψ
        x ← p
        b₁ ← Ο‡ x
        bβ‚‚ ← Ο‡ x
        k x ((a₁ |β†’| bβ‚‚) |∧| True)) β‰‘βŸ¨ a₁ ⇐ Ο• ΝΎ/ sef⟨ψ⟩ _ ⟩
  
    (do a ← Ο•
        x ← p
        b₁ ← Ο‡ x
        bβ‚‚ ← Ο‡ x
        k x ((a |β†’| bβ‚‚) |∧| True)) β‰‘βŸ¨ a ⇐ Ο• ΝΎ/ x ⇐ p ΝΎ/ sef-dsef-cont (Ξ§ x) _ ⟩
  
    (do a ← Ο•
        x ← p
        b ← Ο‡ x
        k x ((a |β†’| b) |∧| True)) β‰‘βŸ¨ a ⇐ Ο• ΝΎ/ x ⇐ p ΝΎ/ b ⇐ Ο‡ x ΝΎ/ cong (k x) (∧-com _ _ ΝΎ ∧-id _) ⟩
  
    (do a ← Ο•
        x ← p
        b ← Ο‡ x
        k x (a |β†’| b)) β‰‘βŸ¨ lhs .proof k ⟩
  
    (do a ← Ο•
        x ← p
        b ← Ο‡ x
        k x True) β‰‘Λ˜βŸ¨ a ⇐ Ο• ΝΎ/ sef⟨ψ⟩ _ ⟩
  
    (do a₁ ← Ο•
        aβ‚‚ ← ψ
        x ← p
        b ← Ο‡ x
        k x True) β‰‘Λ˜βŸ¨ βŸͺassoc⟫ Ο• ψ _|∨|_ _ ⟩
  
    (do a ← Ο• βŸͺ _|∨|_ ⟫ ψ
        x ← p
        b ← Ο‡ x
        k x True) ∎
\end{code}