KM.GHC.same_calcs

From Stdlib Require Import List ListDec Arith Lia Ensembles.
Export ListNotations.

Require Import syntax.
Require Import KMH.
Require Import logics.
Require Import properties.

Section interactions.

    Theorem gKMH_id_KMH : forall Γ A,
        KMH_prv Γ A <-> gKMH_prv Γ A.
    Proof.
    intros Γ A. split.
    + intro D. induction D.
        (* Id *)
        - apply gId ; auto.
        (* Ax *)
        - apply gAx ; auto.
        (* MP *)
        - eapply gMP. exact IHD1. auto.
        (* DN *)
        - apply gNec. apply (gKMH_monot _ _ IHD). intros B HB ; inversion HB.
    + intro D. induction D.
        (* Id *)
        - apply Id ; auto.
        (* Ax *)
        - apply Ax ; auto.
        (* MP *)
        - eapply MP. exact IHD1. auto.
        (* DN *)
        - eapply MP.
          * apply Axcoreflection.
          * exact IHD.
    Qed.

End interactions.