KM.Algebra.KMH_alg_completeness

From Stdlib Require Import Ensembles RelationClasses Morphisms.
Require Import syntax KM_Algebras algebraic_semantic KMH_export.

Completeness of KM w.r.t. algebraic semantic

We prove completeness via the construction of Lindenbaum algebras. To do so, we will use dependent types to capture equivalence classes of formulas.

Section Equiprovable_classes.

We now define the equivalence classes which we use in our Lindenbaum algebra construction.

Variable Γ : @Ensemble form.

Class eqprv : Type :=
  { setform : @Ensemble form ;
    inhab : exists ϕ, setform ϕ ;
    equiprov ϕ : setform ϕ <-> (forall ψ, setform ψ ->
                   (KMH_prv Γ (ψ → ϕ) /\
                    KMH_prv Γ (ϕ → ψ)))
  }.

Equiprovable class of Γ.

Definition sfform_eqprv ϕ := fun ψ => KMH_prv Γ (ϕ → ψ) /\ KMH_prv Γ (ψ → ϕ).

Lemma in_sfform_eqprv ϕ : sfform_eqprv ϕ ϕ.
Proof.
split ; apply imp_Id_gen.
Qed.

Lemma inhabform_eqprv ϕ : exists ψ, sfform_eqprv ϕ ψ.
Proof.
exists ϕ. apply in_sfform_eqprv.
Qed.

Lemma eprvform_eqprv ϕ : forall χ, sfform_eqprv ϕ χ <-> (forall ψ, sfform_eqprv ϕ ψ ->
                   (KMH_prv Γ (ψ → χ) /\
                    KMH_prv Γ (χ → ψ))).
Proof.
intros χ ; split ; intro H.
- intros ψ Hψ ; split ; unfold sfform_eqprv in * ; destruct H ; destruct Hψ.
  + eapply meta_Imp_trans. exact H2. auto.
  + eapply meta_Imp_trans. exact H0. auto.
- split ; apply H ; split ; apply imp_Id_gen.
Qed.

Global Instance epform_eqprv ϕ : eqprv :=
    {|
      setform := sfform_eqprv ϕ ;
      inhab := inhabform_eqprv ϕ ;
      equiprov := eprvform_eqprv ϕ
    |}.

Below is the class for ⊤

Definition sfone := fun ϕ => KMH_prv Γ ϕ.

Lemma inhabone : exists ψ, sfone ψ.
Proof.
exists ⊤. apply prv_Top.
Qed.

Lemma eprvone : forall ϕ, sfone ϕ <-> (forall ψ, sfone ψ ->
                   (KMH_prv Γ (ψ → ϕ) /\
                    KMH_prv Γ (ϕ → ψ))).
Proof.
intros ϕ ; split ; intro H.
- intros ψ Hψ ; split.
  + eapply MP. apply Thm_irrel. auto.
  + eapply MP. apply Thm_irrel. auto.
- destruct (H ⊤).
  + apply prv_Top.
  + eapply MP.
    * exact H0.
    * apply prv_Top.
Qed.

Global Instance epone : eqprv :=
    {|
      setform := sfone ;
      inhab := inhabone ;
      equiprov := eprvone
    |}.

For ⊥.

Definition sfzero := fun ϕ => KMH_prv Γ (ϕ → ⊥).

Lemma inhabzero : exists ψ, sfzero ψ.
Proof.
exists ⊥. apply imp_Id_gen.
Qed.

Lemma eprvzero : forall ϕ, sfzero ϕ <-> (forall ψ, sfzero ψ ->
                   (KMH_prv Γ (ψ → ϕ) /\
                    KMH_prv Γ (ϕ → ψ))).
Proof.
intros ϕ ; split ; intro H.
- intros ψ Hψ ; split.
  + eapply MP. 2: apply EFQ. eapply MP.
    apply Imp_trans. auto.
  + eapply MP. 2: apply EFQ. eapply MP.
    apply Imp_trans. auto.
- destruct (H ⊥) ; auto.
  apply imp_Id_gen.
Qed.

Global Instance epzero : eqprv :=
    {|
      setform := sfzero ;
      inhab := inhabzero ;
      equiprov := eprvzero
    |}.

Join of equivalence classes.

Definition sfjoin (Φ Ψ : eqprv) := fun χ => exists ϕ ψ,
    (@setform Φ) ϕ /\ (@setform Ψ) ψ /\
    KMH_prv Γ ((ϕ ∨ ψ) → χ) /\ KMH_prv Γ (χ → (ϕ ∨ ψ)).

Lemma inhabjoin Φ Ψ : exists ψ, (sfjoin Φ Ψ) ψ.
Proof.
destruct (@inhab Φ) as (ϕ & Hϕ).
destruct (@inhab Ψ) as (ψ & Hψ).
exists (ϕ ∨ ψ). exists ϕ,ψ ; repeat split ; auto ; apply imp_Id_gen.
Qed.

Lemma eprvjoin Φ Ψ : forall ϕ, (sfjoin Φ Ψ) ϕ <-> (forall ψ, (sfjoin Φ Ψ) ψ ->
                   (KMH_prv Γ (ψ → ϕ) /\
                    KMH_prv Γ (ϕ → ψ))).
Proof.
intros χ ; split ; intro H.
- intros δ Hδ ; split.
  + destruct Hδ as (ϕ0 & ψ0 & H0 & H1 & H2 & H3).
    destruct H as (ϕ1 & ψ1 & H4 & H5 & H6 & H7).
    eapply MP.
    * eapply MP.
      -- apply Imp_trans.
      -- exact H3.
    * eapply MP.
      -- eapply MP.
        ++ apply Imp_trans.
        ++ eapply MP.
          ** eapply MP.
            --- apply Ax ; left ; eapply IA5 ; reflexivity.
            --- eapply MP.
              +++ eapply MP.
                *** apply Imp_trans.
                *** rewrite (@equiprov Φ) in H0. apply H0. exact H4.
              +++ apply Ax ; left ; eapply IA3 ; reflexivity.
          ** eapply MP.
            --- eapply MP.
              +++ apply Imp_trans.
              +++ rewrite (@equiprov Ψ) in H1. apply H1. exact H5.
            --- apply Ax ; left ; eapply IA4 ; reflexivity.
      -- auto.
  + destruct Hδ as (ϕ0 & ψ0 & H0 & H1 & H2 & H3).
    destruct H as (ϕ1 & ψ1 & H4 & H5 & H6 & H7).
    eapply MP.
    * eapply MP.
      -- apply Imp_trans.
      -- exact H7.
    * eapply MP.
      -- eapply MP.
        ++ apply Imp_trans.
        ++ eapply MP.
          ** eapply MP.
            --- apply Ax ; left ; eapply IA5 ; reflexivity.
            --- eapply MP.
              +++ eapply MP.
                *** apply Imp_trans.
                *** rewrite (@equiprov Φ) in H4. apply H4. exact H0.
              +++ apply Ax ; left ; eapply IA3 ; reflexivity.
          ** eapply MP.
            --- eapply MP.
              +++ apply Imp_trans.
              +++ rewrite (@equiprov Ψ) in H5. apply H5. exact H1.
            --- apply Ax ; left ; eapply IA4 ; reflexivity.
      -- auto.
- destruct (@inhab Φ) as (ϕ & H1) ; destruct (@inhab Ψ) as (ψ & H2).
  exists ϕ, ψ ; repeat split ; auto.
  + apply H. exists ϕ,ψ ; repeat split ; auto ; apply imp_Id_gen.
  + apply H. exists ϕ,ψ ; repeat split ; auto ; apply imp_Id_gen.
Qed.

Global Instance epjoin Φ Ψ: eqprv :=
    {|
      setform := sfjoin Φ Ψ ;
      inhab := inhabjoin Φ Ψ ;
      equiprov := eprvjoin Φ Ψ
    |}.

Meet of equivalence classes.

Definition sfmeet (Φ Ψ : eqprv) := fun χ => exists ϕ ψ,
    (@setform Φ) ϕ /\ (@setform Ψ) ψ /\
    KMH_prv Γ ((ϕ ∧ ψ) → χ) /\ KMH_prv Γ (χ → (ϕ ∧ ψ)).

Lemma inhabmeet Φ Ψ : exists ψ, (sfmeet Φ Ψ) ψ.
Proof.
destruct (@inhab Φ) as (ϕ & Hϕ).
destruct (@inhab Ψ) as (ψ & Hψ).
exists (ϕ ∧ ψ). exists ϕ,ψ ; repeat split ; auto ; apply imp_Id_gen.
Qed.

Lemma eprvmeet Φ Ψ : forall ϕ, (sfmeet Φ Ψ) ϕ <-> (forall ψ, (sfmeet Φ Ψ) ψ ->
                   (KMH_prv Γ (ψ → ϕ) /\
                    KMH_prv Γ (ϕ → ψ))).
Proof.
intros χ ; split ; intro H.
- intros δ Hδ ; split.
  + destruct Hδ as (ϕ0 & ψ0 & H0 & H1 & H2 & H3).
    destruct H as (ϕ1 & ψ1 & H4 & H5 & H6 & H7).
    eapply MP.
    * eapply MP.
      -- apply Imp_trans.
      -- exact H3.
    * eapply MP.
      -- eapply MP.
        ++ apply Imp_trans.
        ++ eapply MP.
          ** eapply MP.
            --- apply Ax ; left ; eapply IA8 ; reflexivity.
            --- eapply MP.
              +++ eapply MP.
                *** apply Imp_trans.
                *** apply Ax ; left ; eapply IA6 ; reflexivity.
              +++ rewrite (@equiprov Φ) in H0. apply H0. exact H4.
          ** eapply MP.
            --- eapply MP.
              +++ apply Imp_trans.
              +++ apply Ax ; left ; eapply IA7 ; reflexivity.
            --- rewrite (@equiprov Ψ) in H1. apply H1. exact H5.
      -- auto.
  + destruct Hδ as (ϕ0 & ψ0 & H0 & H1 & H2 & H3).
    destruct H as (ϕ1 & ψ1 & H4 & H5 & H6 & H7).
    eapply MP.
    * eapply MP.
      -- apply Imp_trans.
      -- exact H7.
    * eapply MP.
      -- eapply MP.
        ++ apply Imp_trans.
        ++ eapply MP.
          ** eapply MP.
            --- apply Ax ; left ; eapply IA8 ; reflexivity.
            --- eapply MP.
              +++ eapply MP.
                *** apply Imp_trans.
                *** apply Ax ; left ; eapply IA6 ; reflexivity.
              +++ rewrite (@equiprov Φ) in H4. apply H4. exact H0.
          ** eapply MP.
            --- eapply MP.
              +++ apply Imp_trans.
              +++ apply Ax ; left ; eapply IA7 ; reflexivity.
            --- rewrite (@equiprov Ψ) in H5. apply H5. exact H1.
      -- auto.
- destruct (@inhab Φ) as (ϕ & H1) ; destruct (@inhab Ψ) as (ψ & H2).
  exists ϕ, ψ ; repeat split ; auto.
  + apply H. exists ϕ,ψ ; repeat split ; auto ; apply imp_Id_gen.
  + apply H. exists ϕ,ψ ; repeat split ; auto ; apply imp_Id_gen.
Qed.

Global Instance epmeet Φ Ψ: eqprv :=
    {|
      setform := sfmeet Φ Ψ ;
      inhab := inhabmeet Φ Ψ ;
      equiprov := eprvmeet Φ Ψ
    |}.

Implication of equivalence classes.

Definition sfrpc (Φ Ψ : eqprv) := fun χ => exists ϕ ψ,
    (@setform Φ) ϕ /\ (@setform Ψ) ψ /\
    KMH_prv Γ ((ϕ → ψ) → χ) /\ KMH_prv Γ (χ → (ϕ → ψ)).

Lemma inhabrpc Φ Ψ : exists ψ, (sfrpc Φ Ψ) ψ.
Proof.
destruct (@inhab Φ) as (ϕ & Hϕ).
destruct (@inhab Ψ) as (ψ & Hψ).
exists (ϕ → ψ). exists ϕ,ψ ; repeat split ; auto ; apply imp_Id_gen.
Qed.

Lemma eprvrpc Φ Ψ : forall ϕ, (sfrpc Φ Ψ) ϕ <-> (forall ψ, (sfrpc Φ Ψ) ψ ->
                   (KMH_prv Γ (ψ → ϕ) /\
                    KMH_prv Γ (ϕ → ψ))).
Proof.
intros χ ; split ; intro H.
- intros δ Hδ ; split.
  + destruct Hδ as (ϕ0 & ψ0 & H0 & H1 & H2 & H3).
    destruct H as (ϕ1 & ψ1 & H4 & H5 & H6 & H7).
    eapply MP.
    * eapply MP.
      -- apply Imp_trans.
      -- exact H3.
    * eapply MP.
      -- eapply MP.
        ++ apply Imp_trans.
        ++ eapply MP.
          ** apply And_Imp.
          ** eapply MP.
            --- eapply MP.
              +++ apply Imp_trans.
              +++ eapply MP.
                *** eapply MP.
                  ---- apply Imp_trans.
                  ---- eapply MP.
                    ++++ eapply MP.
                      **** apply Ax ; left ; eapply IA8 ; reflexivity.
                      **** apply Ax ; left ; eapply IA6 ; reflexivity.
                    ++++ eapply MP. apply Imp_And. eapply MP.
                         apply Thm_irrel.
                         rewrite (@equiprov Φ) in H4. apply H4. exact H0.
                *** eapply MP.
                    ++++ apply Imp_And.
                    ++++ apply imp_Id_gen.
            --- rewrite (@equiprov Ψ) in H1. apply H1. exact H5.
      -- auto.
  + destruct Hδ as (ϕ0 & ψ0 & H0 & H1 & H2 & H3).
    destruct H as (ϕ1 & ψ1 & H4 & H5 & H6 & H7).
    eapply MP.
    * eapply MP.
      -- apply Imp_trans.
      -- exact H7.
    * eapply MP.
      -- eapply MP.
        ++ apply Imp_trans.
        ++ eapply MP.
          ** apply And_Imp.
          ** eapply MP.
            --- eapply MP.
              +++ apply Imp_trans.
              +++ eapply MP.
                *** eapply MP.
                  ---- apply Imp_trans.
                  ---- eapply MP.
                    ++++ eapply MP.
                      **** apply Ax ; left ; eapply IA8 ; reflexivity.
                      **** apply Ax ; left ; eapply IA6 ; reflexivity.
                    ++++ eapply MP. apply Imp_And. eapply MP.
                         apply Thm_irrel.
                         rewrite (@equiprov Φ) in H0. apply H0. exact H4.
                *** eapply MP.
                    ++++ apply Imp_And.
                    ++++ apply imp_Id_gen.
            --- rewrite (@equiprov Ψ) in H5. apply H5. exact H1.
      -- auto.
- destruct (@inhab Φ) as (ϕ & H1) ; destruct (@inhab Ψ) as (ψ & H2).
  exists ϕ, ψ ; repeat split ; auto.
  + apply H. exists ϕ,ψ ; repeat split ; auto ; apply imp_Id_gen.
  + apply H. exists ϕ,ψ ; repeat split ; auto ; apply imp_Id_gen.
Qed.

Global Instance eprpc Φ Ψ: eqprv :=
    {|
      setform := sfrpc Φ Ψ ;
      inhab := inhabrpc Φ Ψ ;
      equiprov := eprvrpc Φ Ψ
    |}.

Box of equivalence classes.

Definition sfbox (Φ : eqprv) := fun χ => exists ϕ,
    (@setform Φ) ϕ /\
    KMH_prv Γ ((□ ϕ) → χ) /\ KMH_prv Γ (χ → (□ ϕ)).

Lemma inhabbox Φ : exists ψ, (sfbox Φ) ψ.
Proof.
destruct (@inhab Φ) as (ϕ & Hϕ).
exists (□ ϕ). exists ϕ ; repeat split ; auto ; apply imp_Id_gen.
Qed.

Lemma eprvbox Φ : forall ϕ, (sfbox Φ) ϕ <-> (forall ψ, (sfbox Φ) ψ ->
                   (KMH_prv Γ (ψ → ϕ) /\
                    KMH_prv Γ (ϕ → ψ))).
Proof.
intros χ ; split ; intro H.
- intros δ Hδ ; split.
  + destruct Hδ as (ϕ0 & H0 & H1 & H2).
    destruct H as (ϕ1 & H3 & H4 & H5).
    eapply meta_Imp_trans with (□ ϕ1) ; auto.
    eapply meta_Imp_trans with (□ ϕ0) ; auto.
    eapply MP.
    * apply Ax ; right ; eapply K ; reflexivity.
    * apply gKMH_id_KMH. apply gNec. apply gKMH_id_KMH.
      rewrite (@equiprov Φ) in H0. apply H0. exact H3.
  + destruct Hδ as (ϕ0 & H0 & H1 & H2).
    destruct H as (ϕ1 & H3 & H4 & H5).
    eapply meta_Imp_trans with (□ ϕ1) ; auto.
    eapply meta_Imp_trans with (□ ϕ0) ; auto.
    eapply MP.
    * apply Ax ; right ; eapply K ; reflexivity.
    * apply gKMH_id_KMH. apply gNec. apply gKMH_id_KMH.
      rewrite (@equiprov Φ) in H3. apply H3. exact H0.
- destruct (@inhab Φ) as (ϕ & H1).
  exists ϕ ; repeat split ; auto.
  + apply H. exists ϕ ; repeat split ; auto ; apply imp_Id_gen.
  + apply H. exists ϕ ; repeat split ; auto ; apply imp_Id_gen.
Qed.

Global Instance epbox Φ : eqprv :=
    {|
        setform := sfbox Φ ;
        inhab := inhabbox Φ ;
        equiprov := eprvbox Φ
    |}.

End Equiprovable_classes.

Section Properties_eqprv.

Next we show that the operators we just defined on equivalence classes satisfy the algebraic properties of KM-algebras.

Variable Γ : @Ensemble form.

Definition epequiv Φ Ψ := (Same_set form (@setform Γ Φ) (@setform Γ Ψ)).

Infix "≖" := epequiv (at level 70).

Global Instance equiv_epequiv : Equivalence epequiv.
Proof. firstorder. Qed.

Global Instance proper_epmeet : Proper (epequiv ==> epequiv ==> epequiv) (epmeet Γ).
Proof. firstorder. Qed.

Global Instance proper_epjoin : Proper (epequiv ==> epequiv ==> epequiv) (epjoin Γ).
Proof. firstorder. Qed.

Global Instance proper_eprpc : Proper (epequiv ==> epequiv ==> epequiv) (eprpc Γ).
Proof. firstorder. Qed.

Global Instance proper_epbox : Proper (epequiv ==> epequiv) (epbox Γ).
Proof. firstorder. Qed.

Lemma epjcomm Φ Ψ : (epjoin Γ Φ Ψ) ≖ epjoin Γ Ψ Φ.
Proof.
split.
- unfold In in *. unfold setform in * ; cbn in * ; unfold sfjoin in * ; cbn.
  intros A HA.
  destruct HA as (C & D & H0 & H1 & H2 & H3). exists D,C ; repeat split ; auto.
  + eapply MP.
    * eapply MP.
      -- apply Imp_trans.
      -- apply comm_Or_obj.
    * auto.
  + eapply MP.
    * eapply MP.
      -- apply Imp_trans.
      -- exact H3.
    * apply comm_Or_obj.
- unfold In in *. unfold setform in * ; cbn in * ; unfold sfjoin in * ; cbn.
  intros A HA.
  destruct HA as (C & D & H0 & H1 & H2 & H3). exists D,C ; repeat split ; auto.
  + eapply MP.
    * eapply MP.
      -- apply Imp_trans.
      -- apply comm_Or_obj.
    * auto.
  + eapply MP.
    * eapply MP.
      -- apply Imp_trans.
      -- exact H3.
    * apply comm_Or_obj.
Qed.

Lemma epjassoc Φ Ψ Χ : epjoin Γ Φ (epjoin Γ Ψ Χ) ≖ epjoin Γ (epjoin Γ Φ Ψ) Χ.
Proof.
split ; intros A HA.
- unfold In in *. unfold setform in * ; cbn in * ; unfold sfjoin in * ; cbn.
  destruct HA as (C & D & H0 & H1 & H2 & H3).
  unfold setform in * ; cbn in * ; unfold sfjoin in * ; cbn in *.
  destruct H1 as (E & F & H4 & H5 & H6 & H7). unfold setform in *.
  exists (C ∨ E), F ; repeat split ; auto.
  + exists C, E ; repeat split ; auto ; apply imp_Id_gen.
  + eapply MP.
    * eapply MP.
      -- apply Imp_trans.
      -- apply Or_imp_assoc. apply imp_Id_gen.
    * eapply MP.
      -- eapply MP.
        ++ eapply Imp_trans.
        ++ apply monotL_Or. exact H6.
      -- auto.
  + eapply MP.
    * eapply MP.
      -- apply Imp_trans.
      -- exact H3.
    * eapply MP.
      -- eapply MP.
        ++ eapply Imp_trans.
        ++ apply monotL_Or. exact H7.
      -- eapply MP.
        ++ eapply MP.
          ** apply Ax ; left ; eapply IA5 ; reflexivity.
          ** eapply MP.
            --- eapply MP.
              +++ apply Imp_trans.
              +++ apply Ax ; left ; eapply IA3 ; reflexivity.
            --- apply Ax ; left ; eapply IA3 ; reflexivity.
        ++ eapply MP.
          ** eapply MP.
            --- apply Ax ; left ; eapply IA5 ; reflexivity.
            --- eapply MP.
              +++ eapply MP.
                *** apply Imp_trans.
                *** apply Ax ; left ; eapply IA4 ; reflexivity.
              +++ apply Ax ; left ; eapply IA3 ; reflexivity.
          ** apply Ax ; left ; eapply IA4 ; reflexivity.
- unfold In in *. unfold setform in * ; cbn in * ; unfold sfjoin in * ; cbn.
  destruct HA as (C & D & H0 & H1 & H2 & H3).
  unfold setform in * ; cbn in * ; unfold sfjoin in * ; cbn in *.
  destruct H0 as (E & F & H4 & H5 & H6 & H7). unfold setform in *.
  exists E, (F ∨ D) ; repeat split ; auto.
  + exists F, D ; repeat split ; auto ; apply imp_Id_gen.
  + eapply MP.
    * eapply MP.
      -- apply Imp_trans.
      -- eapply MP.
        ++ eapply MP.
          ** apply Ax ; left ; eapply IA5 ; reflexivity.
          ** eapply MP.
            --- eapply MP.
              +++ apply Imp_trans.
              +++ apply Ax ; left ; eapply IA3 ; reflexivity.
            --- apply Ax ; left ; eapply IA3 ; reflexivity.
        ++ eapply MP.
          ** eapply MP.
            --- apply Ax ; left ; eapply IA5 ; reflexivity.
            --- eapply MP.
              +++ eapply MP.
                *** apply Imp_trans.
                *** apply Ax ; left ; eapply IA4 ; reflexivity.
              +++ apply Ax ; left ; eapply IA3 ; reflexivity.
          ** apply Ax ; left ; eapply IA4 ; reflexivity.
    * eapply MP.
      -- eapply MP.
        ++ eapply Imp_trans.
        ++ apply monotR_Or. exact H6.
      -- auto.
  + apply Or_imp_assoc. eapply MP.
    * eapply MP.
      -- apply Imp_trans.
      -- exact H3.
    * apply monotR_Or. auto.
Qed.

Lemma epjabsorp Φ Ψ : epjoin Γ Φ (epmeet Γ Φ Ψ) ≖ Φ.
Proof.
split ; intros A HA.
- unfold In in * ; unfold setform in * ; cbn in * ; unfold sfjoin in * ; cbn.
  destruct HA as (C & D & H0 & H1 & H2 & H3).
  unfold setform in * ; cbn in * ; unfold sfmeet in * ; cbn.
  destruct H1 as (E & F & H4 & H5 & H6 & H7).
  apply equiprov. intros B HB. split.
  + eapply MP.
    * eapply MP.
      -- apply Imp_trans.
      -- rewrite equiprov in HB. apply HB. exact H0.
    * eapply MP.
      -- eapply MP.
        ++ apply Imp_trans.
        ++ apply Ax ; left ; eapply IA3 ; reflexivity.
      -- exact H2.
  + eapply MP.
    * eapply MP.
      -- apply Imp_trans.
      -- exact H3.
    * eapply MP.
      -- eapply MP.
        ++ apply Ax ; left ; eapply IA5 ; reflexivity.
        ++ rewrite equiprov in HB. apply HB. auto.
      -- eapply MP.
        ++ eapply MP.
          ** apply Imp_trans.
          ** exact H7.
        ++ eapply MP.
          ** eapply MP.
            --- eapply Imp_trans.
            --- apply Ax ; left ; eapply IA6 ; reflexivity.
          ** rewrite equiprov in HB. apply HB. auto.
- unfold In in * ; unfold setform in * ; cbn in * ; unfold sfjoin in * ; cbn ;
  unfold sfmeet in * ; cbn in * ; unfold setform in * ; cbn in *.
  destruct (@inhab _ Ψ) as (B & HB).
  exists A, (A ∧ B) ; repeat split ; auto.
  + exists A, B ; repeat split ; auto ; apply imp_Id_gen.
  + eapply MP.
    * eapply MP.
      -- apply Ax ; left ; eapply IA5 ; reflexivity.
      -- apply imp_Id_gen.
    * apply Ax ; left ; eapply IA6 ; reflexivity.
  + apply Ax ; left ; eapply IA3 ; reflexivity.
Qed.

Lemma epmcomm Φ Ψ : epmeet Γ Φ Ψ ≖ epmeet Γ Ψ Φ.
Proof.
split ; intros A HA.
- unfold In in * ; unfold setform in * ; cbn in * ; unfold sfmeet in * ; cbn.
  destruct HA as (C & D & H0 & H1 & H2 & H3). exists D,C ; repeat split ; auto.
  + eapply MP.
    * eapply MP.
      -- apply Imp_trans.
      -- apply comm_And_obj.
    * auto.
  + eapply MP.
    * eapply MP.
      -- apply Imp_trans.
      -- exact H3.
    * apply comm_And_obj.
- unfold In in *. unfold setform in * ; cbn in * ; unfold sfjoin in * ; cbn.
  destruct HA as (C & D & H0 & H1 & H2 & H3). exists D,C ; repeat split ; auto.
  + eapply MP.
    * eapply MP.
      -- apply Imp_trans.
      -- apply comm_And_obj.
    * auto.
  + eapply MP.
    * eapply MP.
      -- apply Imp_trans.
      -- exact H3.
    * apply comm_And_obj.
Qed.

Lemma epmassoc Φ Ψ Χ : epmeet Γ Φ (epmeet Γ Ψ Χ) ≖ epmeet Γ (epmeet Γ Φ Ψ) Χ.
Proof.
 split ; intros A HA.
- unfold In in * ; unfold setform in * ; cbn in * ; unfold sfmeet in * ; cbn.
  destruct HA as (C & D & H0 & H1 & H2 & H3).
  unfold setform in * ; cbn in * ; unfold sfmeet in * ; cbn in *.
  destruct H1 as (E & F & H4 & H5 & H6 & H7). unfold setform in *.
  exists (C ∧ E), F ; repeat split ; auto.
  + exists C, E ; repeat split ; auto ; apply imp_Id_gen.
  + eapply meta_Imp_trans.
    * apply assoc_And_obj.
    * eapply meta_Imp_trans.
      -- eapply MP.
        ++ eapply MP.
          ** apply Ax ; left ; eapply IA8 ; reflexivity.
          ** apply Ax ; left ; eapply IA6 ; reflexivity.
        ++ eapply meta_Imp_trans.
          ** apply Ax ; left ; eapply IA7 ; reflexivity.
          ** exact H6.
      -- auto.
  + eapply meta_Imp_trans.
    * exact H3.
    * eapply MP.
      -- eapply MP.
        ++ apply Ax ; left ; eapply IA8 ; reflexivity.
        ++ eapply MP.
          ** eapply MP.
            --- apply Ax ; left ; eapply IA8 ; reflexivity.
            --- apply Ax ; left ; eapply IA6 ; reflexivity.
          ** eapply meta_Imp_trans.
            --- apply Ax ; left ; eapply IA7 ; reflexivity.
            --- eapply meta_Imp_trans.
              +++ exact H7.
              +++ apply Ax ; left ; eapply IA6 ; reflexivity.
      -- eapply meta_Imp_trans.
        ++ apply Ax ; left ; eapply IA7 ; reflexivity.
        ++ eapply meta_Imp_trans.
          ** exact H7.
          ** apply Ax ; left ; eapply IA7 ; reflexivity.
- unfold In in * ; unfold setform in * ; cbn in * ; unfold sfmeet in * ; cbn.
  destruct HA as (C & D & H0 & H1 & H2 & H3).
  unfold setform in * ; cbn in * ; unfold sfmeet in * ; cbn in *.
  destruct H0 as (E & F & H4 & H5 & H6 & H7). unfold setform in *.
  exists E, (F ∧ D) ; repeat split ; auto.
  + exists F, D ; repeat split ; auto ; apply imp_Id_gen.
  + eapply meta_Imp_trans.
    * apply assoc_And_obj.
    * eapply meta_Imp_trans.
      -- eapply MP.
        ++ eapply MP.
          ** apply Ax ; left ; eapply IA8 ; reflexivity.
          ** eapply meta_Imp_trans.
            --- apply Ax ; left ; eapply IA6 ; reflexivity.
            --- exact H6.
        ++ apply Ax ; left ; eapply IA7 ; reflexivity.
      -- auto.
  + eapply meta_Imp_trans.
    * exact H3.
    * eapply MP.
      -- eapply MP.
        ++ apply Ax ; left ; eapply IA8 ; reflexivity.
        ++ eapply meta_Imp_trans.
          ** apply Ax ; left ; eapply IA6 ; reflexivity.
          ** eapply meta_Imp_trans.
            --- exact H7.
            --- apply Ax ; left ; eapply IA6 ; reflexivity.
      -- eapply MP.
        ++ eapply MP.
          ** apply Ax ; left ; eapply IA8 ; reflexivity.
          ** eapply meta_Imp_trans.
            --- apply Ax ; left ; eapply IA6 ; reflexivity.
            --- eapply meta_Imp_trans.
              +++ exact H7.
              +++ apply Ax ; left ; eapply IA7 ; reflexivity.
        ++ apply Ax ; left ; eapply IA7 ; reflexivity.
Qed.

Lemma epmabsorp Φ Ψ : epmeet Γ Φ (epjoin Γ Φ Ψ) ≖ Φ.
Proof.
split ; intros A HA.
- unfold In in * ; unfold setform in * ; cbn in * ; unfold sfmeet in * ; cbn.
  destruct HA as (C & D & H0 & H1 & H2 & H3).
  unfold setform in * ; cbn in * ; unfold sfjoin in * ; cbn.
  destruct H1 as (E & F & H4 & H5 & H6 & H7).
  apply equiprov. intros B HB. split.
  + eapply meta_Imp_trans. 2: exact H2.
    eapply MP.
    * eapply MP.
      -- apply Ax ; left ; eapply IA8 ; reflexivity.
      -- rewrite equiprov in HB. apply HB. auto.
    * eapply meta_Imp_trans. 2: exact H6.
      eapply meta_Imp_trans.
      -- rewrite equiprov in HB. apply HB. exact H4.
      -- apply Ax ; left ; eapply IA3 ; reflexivity.
  + eapply meta_Imp_trans. exact H3.
    eapply meta_Imp_trans.
    * apply Ax ; left ; eapply IA6 ; reflexivity.
    * rewrite equiprov in HB. apply HB. auto.
- unfold In in * ; unfold setform in * ; cbn in * ; unfold sfmeet in * ; cbn ;
  unfold sfjoin in * ; cbn in * ; unfold setform in * ; cbn in *.
  destruct (@inhab _ Ψ) as (B & HB).
  exists A, (A ∨ B) ; repeat split ; auto.
  + exists A, B ; repeat split ; auto ; apply imp_Id_gen.
  + apply Ax ; left ; eapply IA6 ; reflexivity.
  + eapply MP.
    * eapply MP.
      -- apply Ax ; left ; eapply IA8 ; reflexivity.
      -- apply imp_Id_gen.
    * apply Ax ; left ; eapply IA3 ; reflexivity.
Qed.

Lemma eplowest Φ : epjoin Γ Φ (epzero Γ) ≖ Φ.
Proof.
split ; intros A HA.
- unfold In in * ; unfold setform in * ; cbn in * ; unfold sfjoin in * ; cbn.
  destruct HA as (C & D & H0 & H1 & H2 & H3).
  unfold setform in * ; cbn in * ; unfold sfzero in * ; cbn.
  apply equiprov. intros B HB. split.
  + eapply meta_Imp_trans. 2: exact H2.
    eapply meta_Imp_trans.
    * rewrite equiprov in HB. apply HB. exact H0.
    * apply Ax ; left ; eapply IA3 ; reflexivity.
  + eapply meta_Imp_trans. exact H3.
    eapply MP.
    * eapply MP.
      -- apply Ax ; left ; eapply IA5 ; reflexivity.
      -- rewrite equiprov in HB. apply HB. auto.
    * eapply meta_Imp_trans. exact H1. apply EFQ.
- unfold In in * ; unfold setform in * ; cbn in * ; unfold sfjoin in * ; cbn ;
  unfold sfzero in * ; cbn in * ; unfold setform in * ; cbn in *.
  exists A, ⊥ ; repeat split ; auto.
  + apply imp_Id_gen.
  + eapply MP.
    * eapply MP.
      -- apply Ax ; left ; eapply IA5 ; reflexivity.
      -- apply imp_Id_gen.
    * apply EFQ.
  + apply Ax ; left ; eapply IA3 ; reflexivity.
Qed.

Lemma epgreatest Φ : epmeet Γ Φ (epone Γ) ≖ Φ.
split ; intros A HA.
- unfold In in * ; unfold setform in * ; cbn in * ; unfold sfmeet in * ; cbn.
  destruct HA as (C & D & H0 & H1 & H2 & H3).
  unfold setform in * ; cbn in * ; unfold sfone in * ; cbn.
  apply equiprov. intros B HB. split.
  + eapply meta_Imp_trans. 2: exact H2.
    eapply MP.
    * eapply MP.
      -- apply Ax ; left ; eapply IA8 ; reflexivity.
      -- rewrite equiprov in HB. apply HB. auto.
    * eapply MP. 2: exact H1. apply Thm_irrel.
  + eapply meta_Imp_trans. exact H3.
    eapply meta_Imp_trans.
    * apply Ax ; left ; eapply IA6 ; reflexivity.
    * rewrite equiprov in HB. apply HB. exact H0.
- unfold In in * ; unfold setform in * ; cbn in * ; unfold sfmeet in * ; cbn ;
  unfold sfone in * ; cbn in * ; unfold setform in * ; cbn in *.
  exists A, ⊤ ; repeat split ; auto.
  + apply prv_Top.
  + apply Ax ; left ; eapply IA6 ; reflexivity.
  + eapply MP.
    * eapply MP.
      -- apply Ax ; left ; eapply IA8 ; reflexivity.
      -- apply imp_Id_gen.
    * eapply MP. 2: apply prv_Top. apply Thm_irrel.
Qed.

Lemma epresiduation Φ Ψ Χ : (Φ ≖ epmeet Γ Φ (eprpc Γ Ψ Χ)) <-> (epmeet Γ Φ Ψ ≖ epmeet Γ (epmeet Γ Φ Ψ) Χ).
Proof.
split ; intro H.
- split ; intros A HA.
  + unfold In in * ; unfold setform in * ; cbn in * ; unfold sfmeet in * ; cbn.
    destruct HA as (C & D & H0 & H1 & H2 & H3).
    cbn in * ; unfold sfmeet in * ; cbn.
    destruct Φ. simpl in H.
    apply H in H0. cbn in * ; unfold sfmeet in * ; cbn in *.
    destruct H0 as (E & F & H4 & H5 & H6 & H7).
    unfold sfrpc in * ; cbn in *.
    destruct H5 as (G & K & H8 & H9 & H10 & H11).
    exists (E ∧ G), K. repeat split ; auto.
    * exists E, G ; repeat split ; auto ; apply imp_Id_gen.
    * eapply meta_Imp_trans. 2: exact H2.
      eapply MP.
      -- eapply MP.
        ++ apply Ax ; left ; eapply IA8 ; reflexivity.
        ++ eapply meta_Imp_trans. 2: exact H6.
           eapply meta_Imp_trans. apply assoc_And_obj.
           eapply MP.
          ** eapply MP.
            --- apply Ax ; left ; eapply IA8 ; reflexivity.
            --- apply Ax ; left ; eapply IA6 ; reflexivity.
          ** eapply meta_Imp_trans. 2: exact H10.
             eapply meta_Imp_trans. 2: apply Thm_irrel.
             eapply meta_Imp_trans.
            --- apply Ax ; left ; eapply IA7 ; reflexivity.
            --- apply Ax ; left ; eapply IA7 ; reflexivity.
      -- eapply meta_Imp_trans.
        ++ eapply meta_Imp_trans.
          ** apply Ax ; left ; eapply IA6 ; reflexivity.
          ** apply Ax ; left ; eapply IA7 ; reflexivity.
        ++ rewrite equiprov in H1. apply H1. auto.
    * eapply meta_Imp_trans. exact H3.
      eapply MP.
      -- eapply MP.
        ++ apply Ax ; left ; eapply IA8 ; reflexivity.
        ++ eapply MP.
          ** eapply MP.
            --- apply Ax ; left ; eapply IA8 ; reflexivity.
            --- eapply meta_Imp_trans.
              +++ apply Ax ; left ; eapply IA6 ; reflexivity.
              +++ eapply meta_Imp_trans. exact H7. apply Ax ; left ; eapply IA6 ; reflexivity.
          ** eapply meta_Imp_trans. apply Ax ; left ; eapply IA7 ; reflexivity.
             rewrite equiprov in H1. apply H1. auto.
      -- eapply meta_Imp_trans.
        ++ eapply MP.
          ** eapply MP.
            --- apply Ax ; left ; eapply IA8 ; reflexivity.
            --- eapply meta_Imp_trans.
              +++ apply Ax ; left ; eapply IA6 ; reflexivity.
              +++ eapply meta_Imp_trans.
                *** exact H7.
                *** apply Ax ; left ; eapply IA7 ; reflexivity.
          ** eapply meta_Imp_trans.
            --- apply Ax ; left ; eapply IA7 ; reflexivity.
            --- rewrite equiprov in H1. apply H1. exact H8.
        ++ eapply MP.
          ** apply Imp_And.
          ** auto.
  + unfold In in * ; unfold setform in * ; cbn in * ; unfold sfmeet in * ; cbn.
    destruct HA as (C & D & H0 & H1 & H2 & H3).
    destruct Φ, Ψ.
    cbn in * ; unfold sfmeet in * ; cbn.
    destruct H0 as (E & F & H4 & H5 & H6 & H7).
    cbn in * ; unfold sfmeet in * ; cbn in *. unfold setform in *.
    exists (E ∧ (F → D)), F. repeat split ; auto.
    * apply H. exists E, (F → D) ; repeat split ; auto. 2-3: apply imp_Id_gen.
      exists F,D ; repeat split ; auto ; apply imp_Id_gen.
    * eapply meta_Imp_trans. 2: exact H2.
      eapply MP.
      -- eapply MP.
        ++ apply Ax ; left ; eapply IA8 ; reflexivity.
        ++ eapply meta_Imp_trans. 2: exact H6.
           eapply meta_Imp_trans. apply assoc_And_obj.
           eapply MP.
          ** eapply MP.
            --- apply Ax ; left ; eapply IA8 ; reflexivity.
            --- apply Ax ; left ; eapply IA6 ; reflexivity.
          ** eapply meta_Imp_trans. apply Ax ; left ; eapply IA7 ; reflexivity.
             apply Ax ; left ; eapply IA7 ; reflexivity.
      -- eapply meta_Imp_trans.
        ++ eapply MP.
          ** eapply MP.
            --- apply Ax ; left ; eapply IA8 ; reflexivity.
            --- eapply meta_Imp_trans.
              +++ apply Ax ; left ; eapply IA6 ; reflexivity.
              +++ apply Ax ; left ; eapply IA7 ; reflexivity.
          ** apply Ax ; left ; eapply IA7 ; reflexivity.
        ++ eapply MP.
          ** apply Imp_And.
          ** apply imp_Id_gen.
    * eapply meta_Imp_trans. exact H3.
      eapply MP.
      -- eapply MP.
        ++ apply Ax ; left ; eapply IA8 ; reflexivity.
        ++ eapply MP.
          ** eapply MP.
            --- apply Ax ; left ; eapply IA8 ; reflexivity.
            --- eapply meta_Imp_trans.
              +++ apply Ax ; left ; eapply IA6 ; reflexivity.
              +++ eapply meta_Imp_trans. exact H7. apply Ax ; left ; eapply IA6 ; reflexivity.
          ** eapply meta_Imp_trans. apply Ax ; left ; eapply IA7 ; reflexivity.
             apply Thm_irrel.
      -- eapply meta_Imp_trans.
        ++ apply Ax ; left ; eapply IA6 ; reflexivity.
        ++ eapply meta_Imp_trans.
          ** exact H7.
          ** apply Ax ; left ; eapply IA7 ; reflexivity.
- split ; intros A HA.
  + unfold In in * ; unfold setform in * ; cbn in * ; unfold sfmeet in * ; cbn.
    destruct (@inhab _ Ψ) as (B & HB).
    assert (H1: @setform Γ (epmeet Γ Φ Ψ) (A ∧ B)).
    {
      exists A,B ; repeat split ; auto ; apply imp_Id_gen.
    }
    apply H in H1. cbn in H1.
    destruct H1 as (C & D & H0 & H1 & H2 & H3).
    cbn in * ; unfold sfmeet in * ; cbn.
    destruct H0 as (E & F & H4 & H5 & H6 & H7).
    exists E, (F → D) ; repeat split ; auto.
    * exists F, D ; repeat split ; auto ; apply imp_Id_gen.
    * eapply meta_Imp_trans.
      -- apply Ax ; left ; eapply IA6 ; reflexivity.
      -- rewrite equiprov in H4. apply H4. auto.
    * eapply MP.
      -- eapply MP.
        ++ apply Ax ; left ; eapply IA8 ; reflexivity.
        ++ rewrite equiprov in H4. apply H4. auto.
      -- eapply MP.
        ++ apply And_Imp.
        ++ eapply meta_Imp_trans.
          ** eapply meta_Imp_trans.
            --- eapply MP.
              +++ eapply MP.
                *** apply Ax ; left ; eapply IA8 ; reflexivity.
                *** apply Ax ; left ; eapply IA6 ; reflexivity.
              +++ eapply meta_Imp_trans.
                *** apply Ax ; left ; eapply IA7 ; reflexivity.
                *** rewrite equiprov in HB. apply HB. auto.
            --- exact H3.
          ** apply Ax ; left ; eapply IA7 ; reflexivity.
  + unfold In in * ; unfold setform in * ; cbn in * ; unfold sfmeet in * ; cbn.
    destruct HA as (C & D & H0 & H1 & H2 & H3).
    cbn in * ; unfold sfrpc in * ; cbn.
    destruct H1 as (E & F & H4 & H5 & H6 & H7).
    apply equiprov. intros K HK. split.
    * eapply meta_Imp_trans. 2: exact H2.
      eapply MP.
      -- eapply MP.
        ++ apply Ax ; left ; eapply IA8 ; reflexivity.
        ++ rewrite equiprov in H0. apply H0. auto.
      -- eapply meta_Imp_trans. 2: exact H6.
         eapply MP.
        ++ apply And_Imp.
        ++ assert (H8: @setform Γ (epmeet Γ Φ Ψ) (K ∧ E)).
           { exists K,E ; repeat split ; auto ; apply imp_Id_gen. }
           apply H in H8. unfold setform in H8 ; cbn in H8 ; unfold sfmeet in H8 ; cbn.
           destruct H8 as (J & L & H9 & H10 & H11 & H12).
           eapply meta_Imp_trans.
           ** exact H12.
           ** eapply meta_Imp_trans.
            --- apply Ax ; left ; eapply IA7 ; reflexivity.
            --- eapply equiprov; [apply H10| auto].
    * eapply meta_Imp_trans. exact H3. eapply meta_Imp_trans.
      -- apply Ax ; left ; eapply IA6 ; reflexivity.
      -- rewrite equiprov in H0. apply H0. auto.
Qed.

Lemma epboxone : epbox Γ (epone Γ) ≖ epone Γ.
Proof.
  split ; intros A HA.
  - unfold In in * ; unfold setform in * ; cbn in * ; unfold sfjoin in * ; cbn.
    destruct HA as (C & H & H0 & H2).
    unfold setform in * ; cbn in * ; unfold sfone in * ; cbn.
    eapply MP ; [exact H0 | ]. apply gKMH_id_KMH. apply gNec.
    apply gKMH_id_KMH ; auto.
  - unfold In in * ; unfold setform in * ; cbn in * ; unfold sfbox in * ; cbn ;
    unfold sfone in * ; cbn in * ; unfold setform in * ; cbn in *.
    exists ⊤ ; repeat split ; auto.
    + apply prv_Top.
    + eapply MP.
      * apply Thm_irrel.
      * auto.
    + eapply MP.
      * apply Thm_irrel.
      * apply Nec. apply prv_Top.
Qed.

Lemma epboxnormal Φ Ψ : epbox Γ (epmeet Γ Φ Ψ) ≖ epmeet Γ (epbox Γ Φ) (epbox Γ Ψ).
Proof.
split ; intros A HA.
- unfold In in * ; unfold setform in * ; cbn in * ; unfold sfmeet in * ; cbn ;
  unfold sfbox in * ; cbn in *.
  destruct HA as (C & H0 & H1 & H2).
  unfold setform in * ; cbn in * ; unfold sfmeet in * ; cbn in *.
  destruct H0 as (E & F & H4 & H5 & H6 & H7). unfold setform in *.
  exists (□ E),(□ F). repeat split.
  + exists E. repeat split ; auto ; apply imp_Id_gen.
  + exists F. repeat split ; auto ; apply imp_Id_gen.
  + apply meta_Imp_trans with (□ C) ; auto.
    apply meta_Imp_trans with (□ (E ∧ F)) ; auto.
    * eapply MP. apply Imp_And. repeat apply KMH_Deduction_Theorem.
      apply KMH_monot with
      (fun x : form => exists B : form, In _ (Union form (Singleton _ E) (Singleton _ F)) B /\ x = □ B).
      -- apply K_rule. eapply MP.
        ++ eapply MP.
          ** eapply MP.
            --- apply Ax ; left ; eapply IA8 ; reflexivity.
            --- apply imp_Id_gen.
          ** apply KMH_Deduction_Theorem. apply Id ; left ; right ; split.
        ++ apply Id ; left ; split.
      -- intros D HD. unfold In in *. destruct HD as (P & HP0 & HP1) ; subst.
         inversion HP0 ; subst.
        ++ inversion H ; subst. left ; right ; split.
        ++ inversion H ; subst. right ; split.
    * eapply MP.
      -- apply Ax ; right ; eapply K ; reflexivity.
      -- apply gKMH_id_KMH ; apply gNec ; apply gKMH_id_KMH ; auto.
  + apply meta_Imp_trans with (□ C) ; auto.
    apply meta_Imp_trans with (□ (E ∧ F)) ; auto.
    * eapply MP.
      -- apply Ax ; right ; eapply K ; reflexivity.
      -- apply gKMH_id_KMH ; apply gNec ; apply gKMH_id_KMH ; auto.
    * eapply MP.
      -- eapply MP.
        ++ apply Ax ; left ; eapply IA8 ; reflexivity.
        ++ apply KMH_Deduction_Theorem.
           apply KMH_monot with
           (fun x : form => exists B : form, In _ (Union _ (Empty_set _) (Singleton _ (E ∧ F))) B /\ x = □ B).
          ** apply K_rule. apply KMH_Detachment_Theorem.
             apply Ax ; left ; eapply IA6 ; reflexivity.
          ** intros J HJ ; destruct HJ ; subst. unfold In in *.
             right. destruct H ; subst. inversion H ; subst.
            --- inversion H0.
            --- inversion H0 ; subst. split.
      -- apply KMH_Deduction_Theorem.
         apply KMH_monot with
        (fun x : form => exists B : form, In _ (Union _ (Empty_set _) (Singleton _ (E ∧ F))) B /\ x = □ B).
        ++ apply K_rule. apply KMH_Detachment_Theorem.
           apply Ax ; left ; eapply IA7 ; reflexivity.
        ++ intros J HJ ; destruct HJ ; subst. unfold In in *.
           right. destruct H ; subst. inversion H ; subst.
          ** inversion H0.
          ** inversion H0 ; subst. split.
- unfold In in * ; unfold setform in * ; cbn in * ; unfold sfbox in * ; cbn ;
  unfold sfmeet in * ; cbn in * ; unfold sfbox in * ; cbn in * ; unfold setform in * ; cbn in *.
  destruct HA as (ϕ & ψ & H0 & H1 & H2 & H3).
  destruct H0 as (ϕ0 & H0 & H4 & H5).
  destruct H1 as (ψ0 & H1 & H6 & H7).
  exists (ϕ0 ∧ ψ0) ; repeat split ; auto.
  + exists ϕ0,ψ0. repeat split ; auto. all: apply imp_Id_gen.
  + eapply meta_Imp_trans with (ϕ ∧ ψ) ; auto.
    eapply meta_Imp_trans with ((□ ϕ0) ∧ (□ ψ0)) ; auto.
    * eapply MP.
      -- eapply MP.
        ++ apply Ax ; left ; eapply IA8 ; reflexivity.
        ++ eapply MP ; [ apply Ax ; right ; eapply K ; reflexivity |
           apply gKMH_id_KMH ; apply gNec ; apply gKMH_id_KMH ;
           apply Ax ; left ; eapply IA6 ; reflexivity].
      -- eapply MP ; [ apply Ax ; right ; eapply K ; reflexivity |
         apply gKMH_id_KMH ; apply gNec ; apply gKMH_id_KMH ;
         apply Ax ; left ; eapply IA7 ; reflexivity].
    * eapply MP.
      -- eapply MP.
        ++ apply Ax ; left ; eapply IA8 ; reflexivity.
        ++ eapply meta_Imp_trans with (□ ϕ0) ; auto.
           apply Ax ; left ; eapply IA6 ; reflexivity.
      -- eapply meta_Imp_trans with (□ ψ0) ; auto.
         apply Ax ; left ; eapply IA7 ; reflexivity.
  + eapply meta_Imp_trans with (ϕ ∧ ψ) ; auto.
    eapply meta_Imp_trans with ((□ ϕ0) ∧ (□ ψ0)) ; auto.
    * eapply MP.
      -- eapply MP.
        ++ apply Ax ; left ; eapply IA8 ; reflexivity.
        ++ eapply meta_Imp_trans with ϕ ; auto.
           apply Ax ; left ; eapply IA6 ; reflexivity.
      -- eapply meta_Imp_trans with ψ ; auto.
         apply Ax ; left ; eapply IA7 ; reflexivity.
    * eapply MP.
      -- apply Imp_And.
      -- repeat apply KMH_Deduction_Theorem.
         apply KMH_monot with
         (fun x : form => exists B : form, In _ (Union _ (Empty_set _) (Union _ (Singleton _ ϕ0) (Singleton _ ψ0))) B /\ x = □ B).
         ++ apply K_rule. eapply MP.
          ** eapply MP.
            --- eapply MP.
              +++ apply Ax ; left ; eapply IA8 ; reflexivity.
              +++ apply KMH_Deduction_Theorem. apply Id ; left ; right ; left ; split.
            --- apply KMH_Deduction_Theorem. apply Id ; left ; right ; right ; split.
          ** apply prv_Top.
         ++ intros G HG ; destruct HG. destruct H ; subst.
            destruct H ; try inversion H ; subst. inversion H8 ; subst. left ; right ; split.
            inversion H8 ; subst. right ; split.
Qed.

Lemma epboxcoreflec Φ : Φ ≖ epmeet Γ Φ (epbox Γ Φ).
Proof.
  split ; intros A HA.
  - unfold In in * ; unfold setform in * ; cbn in * ; unfold sfmeet in * ; cbn.
    exists A,(□ A). repeat split ; auto.
    + unfold sfbox. exists A. repeat split ; auto ; apply imp_Id_gen.
    + eapply MP ; [apply Imp_And | ]. apply Thm_irrel.
    + eapply MP.
      * eapply MP.
        -- apply Ax ; left ; eapply IA8 ; reflexivity.
        -- apply imp_Id_gen.
      * apply Axcoreflection.
  - unfold In in * ; unfold setform in * ; cbn in * ; unfold sfmeet in * ; cbn ;
    unfold sfbox in * ; cbn in * ; unfold setform in * ; cbn in *.
    destruct HA as (C & D & H & H0 & H2 & H3).
    unfold sfbox in H0.
    destruct H0 as (F & H4 & H5 & H6).
    apply equiprov. intros. split.
    + apply meta_Imp_trans with (C ∧ D) ; auto.
      apply meta_Imp_trans with (C ∧ (□ F)).
      * eapply MP ; [ eapply MP ; [ apply Ax ; left ; eapply IA8 ; reflexivity | ] | ].
        rewrite equiprov in H0. apply H0 ; auto.
        apply meta_Imp_trans with F ; auto.
        rewrite equiprov in H0. apply H0 ; auto.
        apply Axcoreflection.
      * eapply MP ; [ eapply MP ; [ apply Ax ; left ; eapply IA8 ; reflexivity | ] | ].
        apply Ax ; left ; eapply IA6 ; reflexivity.
        apply meta_Imp_trans with (□ F) ; auto.
        apply Ax ; left ; eapply IA7 ; reflexivity.
    + apply meta_Imp_trans with C.
      * apply meta_Imp_trans with (C ∧ D) ; auto.
        apply Ax ; left ; eapply IA6 ; reflexivity.
      * rewrite equiprov in H0. apply H0 ; auto.
Qed.

Lemma epboxlbx Φ : eprpc Γ (epbox Γ Φ) Φ ≖ Φ.
Proof.
  split ; intros A HA.
  - unfold In in * ; unfold setform in * ; cbn in * ; unfold sfrpc in * ; cbn ;
    unfold sfbox in * ; cbn in * ; cbn in *.
    destruct HA as (C & D & H & H0 & H2 & H3).
    unfold sfbox in H.
    destruct H as (F & H4 & H5 & H6).
    apply equiprov. intros. split.
    + apply meta_Imp_trans with (C → D) ; auto.
      apply meta_Imp_trans with D.
      * rewrite equiprov in H. apply H ; auto.
      * apply Thm_irrel.
    + apply meta_Imp_trans with (C → D) ; auto.
      * apply meta_Imp_trans with ((□ F) → D) ; auto.
        -- apply KMH_Deduction_Theorem.
           apply meta_Imp_trans with C ; auto.
           ++ apply KMH_monot with Γ ; auto.
              intros G HG ; left ; auto.
           ++ apply Id ; right ; split.
        -- apply meta_Imp_trans with F.
           ++ apply meta_Imp_trans with ((□ F) → F) ;
              [ | apply Ax ; right ; eapply L ; reflexivity].
              apply KMH_Deduction_Theorem.
              apply meta_Imp_trans with D.
              ** apply Id ; right ; split.
              ** rewrite equiprov in H0.
                 apply KMH_monot with Γ.
                 apply H0 ; auto.
                 intros G HG ; left ; auto.
           ++ rewrite equiprov in H. apply H ; auto.
  - unfold In in * ; unfold setform in * ; cbn in * ; unfold sfrpc in * ; cbn.
    exists (□ A),A. repeat split ; auto ; [ | apply Ax ; right ; eapply L ; reflexivity | apply Thm_irrel].
    exists A. repeat split ; auto ; apply imp_Id_gen.
Qed.

Lemma epboxnextalw Φ Ψ : epbox Γ Φ ≖ epmeet Γ (epbox Γ Φ) (epjoin Γ Ψ (eprpc Γ Ψ Φ)).
Proof.
  split ; intros A HA.
  - unfold In in * ; unfold setform in * ; cbn in * ; unfold sfbox in * ; cbn ;
    unfold sfmeet in * ; cbn in * ; cbn in *.
    destruct HA as (C & H & H0 & H1).
    exists (□ C).
    destruct (@inhab _ Ψ) as (ψ & Hψ). exists (ψ ∨ (ψ → C)).
    repeat split ; auto.
    + exists C ; repeat split ; auto ; apply imp_Id_gen.
    + exists ψ,(ψ → C). repeat split ; auto. 2,3: apply imp_Id_gen.
      exists ψ,C. repeat split ; auto ; apply imp_Id_gen.
    + apply meta_Imp_trans with (□ C) ; auto.
      apply Ax ; left ; eapply IA6 ; reflexivity.
    + eapply MP ; [ eapply MP ; [ apply Ax ; left ; eapply IA8 ; reflexivity | auto ] | ].
      apply meta_Imp_trans with (□ C) ; auto. apply Ax ; right ; eapply NA ; reflexivity.
  - unfold In in * ; unfold setform in * ; cbn in * ; unfold sfbox in * ; cbn ;
    unfold sfmeet in * ; cbn in * ; cbn in *.
    destruct HA as (C & D & H & H0 & H1 & H2).
    destruct H as (E & H & H3 & H4).
    destruct H0 as (F & G & H0 & H5 & H6 & H7).
    destruct H5 as (I & J & H5 & H8 & H9 & H10).
    exists E. repeat split ; auto.
    + apply meta_Imp_trans with (C ∧ D) ; auto.
      eapply MP ; [ eapply MP ; [ apply Ax ; left ; eapply IA8 ; reflexivity | auto ] | ].
      apply meta_Imp_trans with (F ∨ G) ; auto.
      apply meta_Imp_trans with (F ∨ (I → J)).
      * apply meta_Imp_trans with (F ∨ (F → E)).
        -- apply Ax ; right ; eapply NA ; reflexivity.
        -- eapply MP ; [ eapply MP ; [ apply Ax ; left ; eapply IA5 ; reflexivity | ] | ] .
           apply Ax ; left ; eapply IA3 ; reflexivity.
           apply meta_Imp_trans with (I → J) ; [ | apply Ax ; left ; eapply IA4 ; reflexivity].
           apply KMH_Deduction_Theorem.
           apply meta_Imp_trans with E.
           ++ apply meta_Imp_trans with F ; [ | apply Id ; right ; split].
              apply KMH_monot with Γ. rewrite equiprov in H5 ; apply H5 ; auto.
              intros K HK ; left ; auto.
           ++ apply KMH_monot with Γ. rewrite equiprov in H ; apply H ; auto.
              intros K HK ; left ; auto.
      * eapply MP ; [ eapply MP ; [ apply Ax ; left ; eapply IA5 ; reflexivity | ] | ].
        apply Ax ; left ; eapply IA3 ; reflexivity.
        apply meta_Imp_trans with G ; auto.
        apply Ax ; left ; eapply IA4 ; reflexivity.
    + apply meta_Imp_trans with (C ∧ D) ; auto.
      apply meta_Imp_trans with C ; auto.
      apply Ax ; left ; eapply IA6 ; reflexivity.
Qed.

End Properties_eqprv.

Section Lindenbaum_algebra.

With our equivalence classes, operators on them, and their properties, we can finally build our Lindenbaum algebras.

Variable Γ : @Ensemble form.

    Global Instance LindAlg : KMalg :=
      {|
        nodes := eqprv Γ ;

        equiv := epequiv Γ;
        equiv_equiv := equiv_epequiv Γ ;

        join := epjoin Γ ;
        meet := epmeet Γ ;
        zero := epzero Γ ;
        one := epone Γ ;
        rpc := eprpc Γ ;
        box := epbox Γ ;
        
        proper_meet := proper_epmeet Γ ;
        proper_join := proper_epjoin Γ ;
        proper_rpc := proper_eprpc Γ ;
        proper_box := proper_epbox Γ ;

        jcomm Φ Ψ := epjcomm Γ Φ Ψ ;
        jassoc Φ Ψ Χ := epjassoc Γ Φ Ψ Χ ;
        jabsorp Φ Ψ := epjabsorp Γ Φ Ψ ;
        mcomm Φ Ψ := epmcomm Γ Φ Ψ ;
        massoc Φ Ψ Χ := epmassoc Γ Φ Ψ Χ ;
        mabsorp Φ Ψ := epmabsorp Γ Φ Ψ ;
        lowest Φ := eplowest Γ Φ ;
        greatest Φ := epgreatest Γ Φ ;
        residuation Φ Ψ Χ := epresiduation Γ Φ Ψ Χ ;
        boxone := epboxone Γ ;
        normal Φ Ψ := epboxnormal Γ Φ Ψ ;
        coreflec Φ := epboxcoreflec Γ Φ ;
        lbx Φ := epboxlbx Γ Φ ;
        nextalw Φ Ψ := epboxnextalw Γ Φ Ψ ;
      |}.

Below is the canonical map.

    Definition LindAlgamap (n : nat) := @epform_eqprv Γ (# n).

With the canonical map, we can show that formulas are interpreted by their equivalence classes.

    Lemma LindAlgrepres ϕ : interp LindAlg LindAlgamap ϕ ≡ @epform_eqprv Γ ϕ.
    Proof.
    induction ϕ ; cbn ; auto ; split ; intros A HA ;
    unfold In in * ; unfold setform in * ; cbn in *.
    - split; apply HA.
    - split; apply HA.
    (* ⊥ *)
    - split ; auto. apply EFQ.
    - destruct HA ; auto.
    (* ∧ *)
    - split.
      + destruct HA as (B & C & H0 & H1 & H2 & H3). eapply meta_Imp_trans. 2: exact H2.
        eapply MP.
        * eapply MP.
          -- apply Ax ; left ; eapply IA8 ; reflexivity.
          -- eapply meta_Imp_trans.
            ++ apply Ax ; left ; eapply IA6 ; reflexivity.
            ++ rewrite equiprov in H0. apply H0. apply IHϕ1, in_sfform_eqprv.
        * eapply meta_Imp_trans.
          -- apply Ax ; left ; eapply IA7 ; reflexivity.
          -- rewrite equiprov in H1. apply H1, IHϕ2, in_sfform_eqprv.
      + destruct HA as (B & C & H0 & H1 & H2 & H3). eapply meta_Imp_trans. exact H3.
        eapply MP.
        * eapply MP.
          -- apply Ax ; left ; eapply IA8 ; reflexivity.
          -- eapply meta_Imp_trans.
            ++ apply Ax ; left ; eapply IA6 ; reflexivity.
            ++ rewrite equiprov in H0. apply H0, IHϕ1, in_sfform_eqprv.
        * eapply meta_Imp_trans.
          -- apply Ax ; left ; eapply IA7 ; reflexivity.
          -- rewrite equiprov in H1. apply H1, IHϕ2, in_sfform_eqprv.
    - exists ϕ1,ϕ2 ; repeat split ; try solve[destruct HA ; auto].
      + apply IHϕ1, in_sfform_eqprv.
      + apply IHϕ2, in_sfform_eqprv.
    (* ∨ *)
    - split.
      + destruct HA as (B & C & H0 & H1 & H2 & H3). eapply meta_Imp_trans. 2: exact H2.
        eapply MP.
        * eapply MP.
          -- apply Ax ; left ; eapply IA5 ; reflexivity.
          -- eapply meta_Imp_trans.
            ++ rewrite equiprov in H0. apply H0, IHϕ1, in_sfform_eqprv.
            ++ apply Ax ; left ; eapply IA3 ; reflexivity.
        * eapply meta_Imp_trans.
          -- rewrite equiprov in H1. apply H1, IHϕ2, in_sfform_eqprv.
          -- apply Ax ; left ; eapply IA4 ; reflexivity.
      + destruct HA as (B & C & H0 & H1 & H2 & H3). eapply meta_Imp_trans. exact H3.
        eapply MP.
        * eapply MP.
          -- apply Ax ; left ; eapply IA5 ; reflexivity.
          -- eapply meta_Imp_trans.
            ++ rewrite equiprov in H0. apply H0, IHϕ1, in_sfform_eqprv.
            ++ apply Ax ; left ; eapply IA3 ; reflexivity.
        * eapply meta_Imp_trans.
          -- rewrite equiprov in H1. apply H1, IHϕ2, in_sfform_eqprv.
          -- apply Ax ; left ; eapply IA4 ; reflexivity.
    - exists ϕ1,ϕ2 ; repeat split ; try solve[destruct HA ; auto].
      + apply IHϕ1, in_sfform_eqprv.
      + apply IHϕ2, in_sfform_eqprv.
    (* → *)
    - split.
      + destruct HA as (B & C & H0 & H1 & H2 & H3). eapply meta_Imp_trans. 2: exact H2.
        eapply MP. apply And_Imp. eapply meta_Imp_trans.
        * eapply meta_Imp_trans.
          -- eapply MP.
            ++ eapply MP.
              ** apply Ax ; left ; eapply IA8 ; reflexivity.
              ** apply Ax ; left ; eapply IA6 ; reflexivity.
            ++ eapply meta_Imp_trans.
              ** apply Ax ; left ; eapply IA7 ; reflexivity.
              ** rewrite equiprov in H0. apply H0,IHϕ1, in_sfform_eqprv.
          -- eapply MP. apply Imp_And. apply imp_Id_gen.
        * rewrite equiprov in H1. apply H1, IHϕ2, in_sfform_eqprv.
      + destruct HA as (B & C & H0 & H1 & H2 & H3). eapply meta_Imp_trans. exact H3.
        eapply MP. apply And_Imp. eapply meta_Imp_trans.
        * eapply meta_Imp_trans.
          -- eapply MP.
            ++ eapply MP.
              ** apply Ax ; left ; eapply IA8 ; reflexivity.
              ** apply Ax ; left ; eapply IA6 ; reflexivity.
            ++ eapply meta_Imp_trans.
              ** apply Ax ; left ; eapply IA7 ; reflexivity.
              ** rewrite equiprov in H0. apply H0,IHϕ1, in_sfform_eqprv.
          -- eapply MP. apply Imp_And. apply imp_Id_gen.
        * rewrite equiprov in H1. apply H1, IHϕ2, in_sfform_eqprv.
    - exists ϕ1,ϕ2 ; repeat split ; try solve[destruct HA ; auto].
      + apply IHϕ1, in_sfform_eqprv.
      + apply IHϕ2, in_sfform_eqprv.
    (* □ *)
    - split.
      + destruct HA as (B & H0 & H1 & H2). eapply meta_Imp_trans with (□ B) ; auto.
        eapply MP ; [ apply Ax ; right ; eapply K ; reflexivity | ].
        apply gKMH_id_KMH. apply gNec. apply gKMH_id_KMH.
        rewrite equiprov in H0. apply H0, IHϕ, in_sfform_eqprv.
      + destruct HA as (B & H0 & H1 & H2). apply meta_Imp_trans with (□ B) ; auto.
        eapply MP ; [ apply Ax ; right ; eapply K ; reflexivity | ].
        apply gKMH_id_KMH. apply gNec. apply gKMH_id_KMH.
        rewrite equiprov in H0. apply H0, IHϕ, in_sfform_eqprv.
    - exists ϕ ; repeat split ; try solve[destruct HA ; auto].
      apply IHϕ, in_sfform_eqprv.
    Qed.

End Lindenbaum_algebra.

Section Completeness.

We finish by showing the completeness result, which follows from the properties of our Lindenbaum algebras.

Definition sEq ϕ ψ := ϕ = # 0 /\ ψ = ⊤.

Variable Γ : @Ensemble form.

Theorem alg_completeness_KMH ϕ : alg_eqconseq sEq Γ ϕ -> KMH_prv Γ ϕ.
Proof.
intro H.
assert (K: sEq # 0 ⊤). split ; auto.
pose (H _ _ K (LindAlg Γ) (LindAlgamap Γ)). cbn in e.
pose (Top_rpczz (LindAlg Γ)) as eone.
cbn in eone. rewrite <- eone in e.
rewrite LindAlgrepres in *.
assert (H0 : epequiv Γ (epform_eqprv Γ ϕ) (epone Γ)).
{
  apply e. intros χ δ H0.
  destruct H0 as (C & D & H1 & E & H3 & H4 & H5) ; subst. inversion H1 ; subst.
  cbn. rewrite LindAlgrepres. rewrite <- eone.
  split ; intros A HA ; unfold In in * ;
  unfold setform in * ; cbn in *.
  - destruct HA. eapply MP.
    + exact H0.
    + apply Id ; auto.
  - split.
    + eapply MP. apply Thm_irrel. auto.
    + eapply MP. apply Thm_irrel. apply Id ; auto.
}
assert (@setform _ (epone Γ) ϕ).
{
  apply H0, in_sfform_eqprv.
}
auto.
Qed.

End Completeness.