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

open import Prelude renaming (tt to ⟨⟩)
open import Signatures
open import FinitenessConditions
open import FreeMonad.PackagedTheory
open import FreeMonad.FindVars using (FindVars)
open import Finite using (β„°)

module Hoare.HElim (𝒯 : FullTheory β„“zero)
                   (findVar : FindVars (FullTheory.𝒯 𝒯))
                   (fin-arities : βˆ€ Oα΅’ β†’ β„° (Signature.Arity (FullTheory.𝔽 𝒯) Oα΅’)) where

open import Truth using (ProofOf ; _|β†’|_ ; |β†’|-idΛ‘; True; Ξ©)
open import Hoare.Definition 𝒯
open import FreeMonad.HElim 𝒯 findVar fin-arities
open import FreeMonad.Quotiented 𝒯

module _ {p : Level} where
  -- open import Truth.MonoLevel p
  -- open DisplayGlobal {p}

  -- This is just 𝒒-elim repackaged for Hoare logic
  module _ {A B : Type}
           (Ο• : A β†’ Ξ© p)
           (f g : A β†’ Term B)
           (k : (x : A) β†’ ProofOf (Ο• x) β†’ f x ≑ g x)
           (t : Term A) where
\end{code}

%<*h-elim>
\begin{code}
    H-elim  : (βŸ…βŸ† x ← t βŸ… return (Ο• x) βŸ†) β†’ (t >>= f) ≑ (t >>= g)
\end{code}
%</h-elim>

\begin{code}
    H-elim h = 𝒒-elim Ο• f g k t $
      Ο•? Ο• <$> t β‰‘βŸ¨βŸ©
      (do x ← t; return (x , Ο• x)) β‰‘βŸ¨ x ⇐ t ΝΎ/ cong (return ∘ (_,_ x)) (const Truth.iff Ξ» f β†’ f _) ⟩
      (do x ← t; return (x , True |β†’| Ο• x)) β‰‘βŸ¨ on-pair h ⟩
      (do x ← t; return (x , True)) β‰‘βŸ¨βŸ©
      Ο•T Ο• <$> t ∎
\end{code}