Require Import Logic.lib.Coqlib.
Require Import Logic.lib.Ensembles_ext.
Require Import Logic.GeneralLogic.Base.
Require Import Logic.GeneralLogic.ProofTheory.TheoryOfSequentCalculus.
Require Import Logic.GeneralLogic.ProofTheory.BasicSequentCalculus.
Require Import Logic.MinimunLogic.Syntax.
Require Import Logic.MinimunLogic.ProofTheory.TheoryOfSequentCalculus.

Local Open Scope logic_base.
Local Open Scope syntax.

(* Goal: DeductionWeaken L Gamma *)
(* Goal: BasicSequentCalculus L Gamma *)
Definition multi_imp {L: Language} {minL: MinimunLanguage L} (xs: list expr) (y: expr): expr :=
  fold_right impp y xs.

(* Goal: DeductionWeaken L Gamma *)
(* Goal: BasicSequentCalculus L Gamma *)
Class NormalAxiomatization (L: Language) {minL: MinimunLanguage L} (Gamma: ProofTheory L): Type := {
  derivable_provable: forall Phi y, derivable Phi y <->
                        exists xs, Forall (fun x => Phi x) xs /\ provable (multi_imp xs y)
}.

(* Goal: DeductionWeaken L Gamma *)
(* Goal: BasicSequentCalculus L Gamma *)
Class MinimunAxiomatization (L: Language) {minL: MinimunLanguage L} (Gamma: ProofTheory L) := {
  modus_ponens: forall x y, |-- (x --> y) -> |-- x -> |-- y;
  axiom1: forall x y, |-- (x --> (y --> x));
  axiom2: forall x y z, |-- ((x --> y --> z) --> (x --> y) --> (x --> z))
}.

(* Goal: DeductionWeaken L Gamma *)
(* Goal: BasicSequentCalculus L Gamma *)
Class MinimunSequentCalculus (L: Language) {minL: MinimunLanguage L} (Gamma: ProofTheory L) := {
  deduction_modus_ponens: forall Phi x y, Phi |-- x -> Phi |-- x --> y -> Phi |-- y;
  deduction_impp_intros: forall Phi x y, Phi;; x |-- y -> Phi |-- x --> y
}.

Section DerivableRulesFromAxiomatization.

(* Goal: DeductionWeaken L Gamma *)
(* Goal: BasicSequentCalculus L Gamma *)
Context {L: Language}
(* Goal: DeductionWeaken L Gamma *)
(* Goal: BasicSequentCalculus L Gamma *)
        {minL: MinimunLanguage L}
(* Goal: DeductionWeaken L Gamma *)
(* Goal: BasicSequentCalculus L Gamma *)
        {Gamma: ProofTheory L}
(* Goal: DeductionWeaken L Gamma *)
(* Goal: BasicSequentCalculus L Gamma *)
        {minAX: MinimunAxiomatization L Gamma}.

Lemma provable_impp_refl: forall (x: expr), |-- x --> x.
Proof.
(* Goal: forall (G : Prop) (l : list (@sig Prop (fun X : Prop => X))), iff (forall (_ : FiniteWitnessedSequentCalculus L (@Build_SequentCalculus L (@derivable L Gamma))) (_ : @NormalAxiomatization L minL (@Build_SequentCalculus L (@derivable L Gamma))) (_ : Typeclass_Rewrite l), G) (forall _ : Typeclass_Rewrite (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (FiniteWitnessedSequentCalculus L Gamma) fwSC) l), G) *)
  intros.
(* Goal: @provable L Gamma (@impp L minL x x) *)
  pose proof axiom2 x (x --> x) x.
(* Goal: @provable L Gamma (@impp L minL x x) *)
  pose proof axiom1 x (x --> x).
(* Goal: @provable L Gamma (@impp L minL x x) *)
  pose proof axiom1 x x.
(* Goal: @provable L Gamma (@impp L minL (@impp L minL x (@impp L minL x y)) (@impp L minL x y)) *)
  pose proof modus_ponens _ _ H H0.
(* Goal: @provable L Gamma (@impp L minL x x) *)
  pose proof modus_ponens _ _ H2 H1.
(* Goal: forall (a : @expr L) (_ : Phi a), Psi a *)
  auto.
Qed.

Lemma aux_minimun_rule00: forall (x y: expr), |-- x -> |-- y --> x.
Proof.
(* Goal: forall (G : Prop) (l : list (@sig Prop (fun X : Prop => X))), iff (forall (_ : FiniteWitnessedSequentCalculus L (@Build_SequentCalculus L (@derivable L Gamma))) (_ : @NormalAxiomatization L minL (@Build_SequentCalculus L (@derivable L Gamma))) (_ : Typeclass_Rewrite l), G) (forall _ : Typeclass_Rewrite (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (FiniteWitnessedSequentCalculus L Gamma) fwSC) l), G) *)
  intros.
  pose proof axiom1 x y.
(* Goal: forall (a : @expr L) (_ : Phi a), Psi a *)
  eapply modus_ponens; eauto.
Qed.

Lemma aux_minimun_theorem00: forall (x y z: expr), |--  (y --> z) --> (x --> y) --> (x --> z).
Proof.
(* Goal: forall (G : Prop) (l : list (@sig Prop (fun X : Prop => X))), iff (forall (_ : FiniteWitnessedSequentCalculus L (@Build_SequentCalculus L (@derivable L Gamma))) (_ : @NormalAxiomatization L minL (@Build_SequentCalculus L (@derivable L Gamma))) (_ : Typeclass_Rewrite l), G) (forall _ : Typeclass_Rewrite (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (FiniteWitnessedSequentCalculus L Gamma) fwSC) l), G) *)
  intros.
(* Goal: @provable L Gamma (@impp L minL (@impp L minL y z) (@impp L minL (@impp L minL x y) (@impp L minL x z))) *)
  pose proof axiom2 x y z.
(* Goal: @provable L Gamma (@impp L minL (@impp L minL y z) (@impp L minL (@impp L minL x y) (@impp L minL x z))) *)
  pose proof aux_minimun_rule00 _ (y --> z) H.
(* Goal: @provable L Gamma (@impp L minL (@impp L minL y z) (@impp L minL (@impp L minL x y) (@impp L minL x z))) *)
  pose proof axiom1 (y --> z) x.
(* Goal: @provable L Gamma (@impp L minL (@impp L minL y z) (@impp L minL (@impp L minL x y) (@impp L minL x z))) *)
  pose proof axiom2 (y --> z) (x --> y --> z) ((x --> y) --> (x --> z)).
(* Goal: @provable L Gamma (@impp L minL (@impp L minL y z) (@impp L minL (@impp L minL x y) (@impp L minL x z))) *)
  pose proof modus_ponens _ _ H2 H0.
(* Goal: @provable L Gamma (@impp L minL (@impp L minL y z) (@impp L minL (@impp L minL x y) (@impp L minL x z))) *)
  pose proof modus_ponens _ _ H3 H1.
(* Goal: forall (a : @expr L) (_ : Phi a), Psi a *)
  auto.
Qed.

Lemma aux_minimun_rule01: forall (x y z: expr), |-- x --> y -> |-- (z --> x) --> (z --> y).
Proof.
(* Goal: forall (G : Prop) (l : list (@sig Prop (fun X : Prop => X))), iff (forall (_ : FiniteWitnessedSequentCalculus L (@Build_SequentCalculus L (@derivable L Gamma))) (_ : @NormalAxiomatization L minL (@Build_SequentCalculus L (@derivable L Gamma))) (_ : Typeclass_Rewrite l), G) (forall _ : Typeclass_Rewrite (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (FiniteWitnessedSequentCalculus L Gamma) fwSC) l), G) *)
  intros.
(* Goal: @provable L Gamma (@impp L minL (@impp L minL z x) (@impp L minL z y)) *)
  pose proof aux_minimun_theorem00 z x y.
(* Goal: @provable L Gamma (@impp L minL (@impp L minL z x) (@impp L minL z y)) *)
  pose proof modus_ponens _ _ H0 H.
(* Goal: forall (a : @expr L) (_ : Phi a), Psi a *)
  auto.
Qed.

Lemma aux_minimun_rule02: forall (x y z: expr), |-- x --> y -> |-- y --> z -> |-- x --> z.
Proof.
(* Goal: forall (G : Prop) (l : list (@sig Prop (fun X : Prop => X))), iff (forall (_ : FiniteWitnessedSequentCalculus L (@Build_SequentCalculus L (@derivable L Gamma))) (_ : @NormalAxiomatization L minL (@Build_SequentCalculus L (@derivable L Gamma))) (_ : Typeclass_Rewrite l), G) (forall _ : Typeclass_Rewrite (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (FiniteWitnessedSequentCalculus L Gamma) fwSC) l), G) *)
  intros.
(* Goal: @provable L Gamma (@impp L minL x z) *)
  pose proof aux_minimun_theorem00 x y z.
(* Goal: @provable L Gamma (@impp L minL x z) *)
  pose proof modus_ponens _ _ H1 H0.
(* Goal: @provable L Gamma (@impp L minL x z) *)
  pose proof modus_ponens _ _ H2 H.
(* Goal: forall (a : @expr L) (_ : Phi a), Psi a *)
  auto.
Qed.

Lemma aux_minimun_theorem01: forall (x y z: expr), |-- (x --> z) --> (x --> y --> z).
Proof.
(* Goal: forall (G : Prop) (l : list (@sig Prop (fun X : Prop => X))), iff (forall (_ : FiniteWitnessedSequentCalculus L (@Build_SequentCalculus L (@derivable L Gamma))) (_ : @NormalAxiomatization L minL (@Build_SequentCalculus L (@derivable L Gamma))) (_ : Typeclass_Rewrite l), G) (forall _ : Typeclass_Rewrite (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (FiniteWitnessedSequentCalculus L Gamma) fwSC) l), G) *)
  intros.
(* Goal: @provable L Gamma (@impp L minL (@impp L minL a (@multi_imp L minL xs y)) (@impp L minL a (@impp L minL a (@impp L minL (@impp L minL a (@multi_imp L minL xs (@impp L minL y z))) (@multi_imp L minL xs z))))) *)
  apply aux_minimun_rule01.
(* Goal: @provable L Gamma (@impp L minL (@multi_imp L minL (@nil (@expr L)) y) (@impp L minL x y)) *)
  apply axiom1.
Qed.

Lemma aux_minimun_theorem02: forall (x y: expr), |-- x --> (x --> y) --> y.
Proof.
(* Goal: forall (G : Prop) (l : list (@sig Prop (fun X : Prop => X))), iff (forall (_ : FiniteWitnessedSequentCalculus L (@Build_SequentCalculus L (@derivable L Gamma))) (_ : @NormalAxiomatization L minL (@Build_SequentCalculus L (@derivable L Gamma))) (_ : Typeclass_Rewrite l), G) (forall _ : Typeclass_Rewrite (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (FiniteWitnessedSequentCalculus L Gamma) fwSC) l), G) *)
  intros.
(* Goal: @provable L Gamma (@impp L minL x (@impp L minL (@impp L minL x y) y)) *)
  pose proof axiom2 (x --> y) x y.
(* Goal: @provable L Gamma (@impp L minL x (@impp L minL (@impp L minL x y) y)) *)
  pose proof provable_impp_refl (x --> y).
(* Goal: @provable L Gamma (@impp L minL (@impp L minL x (@impp L minL x y)) (@impp L minL x y)) *)
  pose proof modus_ponens _ _ H H0.
(* Goal: @provable L Gamma (@impp L minL x (@impp L minL (@impp L minL x y) y)) *)
  pose proof aux_minimun_rule01 _ _ x H1.
(* Goal: @provable L Gamma (@impp L minL x (@impp L minL (@impp L minL x y) y)) *)
  pose proof axiom1 x (x --> y).
(* Goal: @provable L Gamma (@impp L minL x (@impp L minL (@impp L minL x y) y)) *)
  pose proof modus_ponens _ _ H2 H3.
(* Goal: forall (a : @expr L) (_ : Phi a), Psi a *)
  auto.
Qed.

Lemma aux_minimun_theorem03: forall (x y z: expr), |--  y --> (x --> y --> z) --> (x --> z).
Proof.
(* Goal: forall (G : Prop) (l : list (@sig Prop (fun X : Prop => X))), iff (forall (_ : FiniteWitnessedSequentCalculus L (@Build_SequentCalculus L (@derivable L Gamma))) (_ : @NormalAxiomatization L minL (@Build_SequentCalculus L (@derivable L Gamma))) (_ : Typeclass_Rewrite l), G) (forall _ : Typeclass_Rewrite (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (FiniteWitnessedSequentCalculus L Gamma) fwSC) l), G) *)
  intros.
(* Goal: @provable L Gamma (@impp L minL y (@impp L minL (@impp L minL x (@impp L minL y z)) (@impp L minL x z))) *)
  pose proof aux_minimun_theorem00 x (y --> z) z.
(* Goal: @provable L Gamma (@impp L minL y (@impp L minL (@impp L minL x (@impp L minL y z)) (@impp L minL x z))) *)
  pose proof aux_minimun_theorem02 y z.
(* Goal: forall (a : @expr L) (_ : Phi a), Psi a *)
  eapply aux_minimun_rule02; eauto.
Qed.

Lemma aux_minimun_theorem04: forall (x y: expr), |-- (x --> x --> y) --> x --> y.
Proof.
(* Goal: forall (G : Prop) (l : list (@sig Prop (fun X : Prop => X))), iff (forall (_ : FiniteWitnessedSequentCalculus L (@Build_SequentCalculus L (@derivable L Gamma))) (_ : @NormalAxiomatization L minL (@Build_SequentCalculus L (@derivable L Gamma))) (_ : Typeclass_Rewrite l), G) (forall _ : Typeclass_Rewrite (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (FiniteWitnessedSequentCalculus L Gamma) fwSC) l), G) *)
  intros.
(* Goal: @provable L Gamma (@impp L minL (@impp L minL x (@impp L minL x y)) (@impp L minL x y)) *)
  pose proof axiom2 x (x --> y) y.
(* Goal: @provable L Gamma (@impp L minL (@impp L minL x (@impp L minL x y)) (@impp L minL x y)) *)
  pose proof aux_minimun_theorem02 x y.
(* Goal: @provable L Gamma (@impp L minL (@impp L minL x (@impp L minL x y)) (@impp L minL x y)) *)
  pose proof modus_ponens _ _ H H0.
(* Goal: forall (a : @expr L) (_ : Phi a), Psi a *)
  auto.
Qed.

Lemma provable_impp_arg_switch: forall (x y z: expr), |-- (x --> y --> z) --> (y --> x --> z).
Proof.
(* Goal: forall (G : Prop) (l : list (@sig Prop (fun X : Prop => X))), iff (forall (_ : FiniteWitnessedSequentCalculus L (@Build_SequentCalculus L (@derivable L Gamma))) (_ : @NormalAxiomatization L minL (@Build_SequentCalculus L (@derivable L Gamma))) (_ : Typeclass_Rewrite l), G) (forall _ : Typeclass_Rewrite (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (FiniteWitnessedSequentCalculus L Gamma) fwSC) l), G) *)
  intros.
(* Goal: @provable L Gamma (@impp L minL (@impp L minL x (@impp L minL y z)) (@impp L minL y (@impp L minL x z))) *)
  apply aux_minimun_rule02 with (y --> x --> y --> z).
(* Goal: @provable L Gamma (@impp L minL (@multi_imp L minL (@nil (@expr L)) y) (@impp L minL x y)) *)
  + apply axiom1.
  + pose proof axiom2 y (x --> y --> z) (x --> z).
(* Goal: forall (a : @expr L) (_ : Phi a), Psi a *)
    eapply modus_ponens; eauto. clear H.
(* Goal: @provable L Gamma (@impp L minL y (@impp L minL (@impp L minL x (@impp L minL y z)) (@impp L minL x z))) *)
    pose proof aux_minimun_theorem00 x (y --> z) z.
(* Goal: forall (a : @expr L) (_ : Phi a), Psi a *)
    eapply aux_minimun_rule02; eauto.
(* Goal: @provable L Gamma (@impp L minL y (@impp L minL (@impp L minL y z) z)) *)
    apply aux_minimun_theorem02.
Qed.

Lemma provable_impp_trans: forall (x y z: expr), |-- (x --> y) --> (y --> z) --> (x --> z).
Proof.
(* Goal: forall (G : Prop) (l : list (@sig Prop (fun X : Prop => X))), iff (forall (_ : FiniteWitnessedSequentCalculus L (@Build_SequentCalculus L (@derivable L Gamma))) (_ : @NormalAxiomatization L minL (@Build_SequentCalculus L (@derivable L Gamma))) (_ : Typeclass_Rewrite l), G) (forall _ : Typeclass_Rewrite (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (FiniteWitnessedSequentCalculus L Gamma) fwSC) l), G) *)
  intros.
(* Goal: @provable L Gamma (@impp L minL (@impp L minL x y) (@impp L minL (@impp L minL y z) (@impp L minL x z))) *)
  pose proof provable_impp_arg_switch (y --> z) (x --> y) (x --> z).
(* Goal: forall (a : @expr L) (_ : Phi a), Psi a *)
  eapply modus_ponens; eauto. clear H.
(* Goal: @provable L Gamma (@impp L minL (@impp L minL (@multi_imp L minL xs (@impp L minL y z)) (@multi_imp L minL xs z)) (@impp L minL (@impp L minL a (@multi_imp L minL xs (@impp L minL y z))) (@impp L minL a (@multi_imp L minL xs z)))) *)
  apply aux_minimun_theorem00.
Qed.

End DerivableRulesFromAxiomatization.

Section DerivableRules_multi_impp.

(* Goal: DeductionWeaken L Gamma *)
(* Goal: BasicSequentCalculus L Gamma *)
Context {L: Language}
(* Goal: DeductionWeaken L Gamma *)
(* Goal: BasicSequentCalculus L Gamma *)
        {minL: MinimunLanguage L}
(* Goal: DeductionWeaken L Gamma *)
(* Goal: BasicSequentCalculus L Gamma *)
        {Gamma: ProofTheory L}
(* Goal: DeductionWeaken L Gamma *)
(* Goal: BasicSequentCalculus L Gamma *)
        {minAX: MinimunAxiomatization L Gamma}.

Lemma provable_multi_imp_shrink: forall (xs: list expr) (x y: expr), |-- (x --> multi_imp xs (x --> y)) --> multi_imp xs (x --> y).
Proof.
(* Goal: forall (G : Prop) (l : list (@sig Prop (fun X : Prop => X))), iff (forall (_ : FiniteWitnessedSequentCalculus L (@Build_SequentCalculus L (@derivable L Gamma))) (_ : @NormalAxiomatization L minL (@Build_SequentCalculus L (@derivable L Gamma))) (_ : Typeclass_Rewrite l), G) (forall _ : Typeclass_Rewrite (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (FiniteWitnessedSequentCalculus L Gamma) fwSC) l), G) *)
  intros.
(* Goal: @provable L Gamma (@impp L minL (@multi_imp L minL xs x) (@multi_imp L minL xs y)) *)
  induction xs.
  + simpl.
(* Goal: @provable L Gamma (@impp L minL (@impp L minL x (@impp L minL x y)) (@impp L minL x y)) *)
    apply aux_minimun_theorem04.
  + simpl.
(* Goal: @provable L Gamma (@impp L minL (@impp L minL x (@impp L minL a (@multi_imp L minL xs (@impp L minL x y)))) (@impp L minL a (@multi_imp L minL xs (@impp L minL x y)))) *)
    apply aux_minimun_rule01 with (z := a) in IHxs.
(* Goal: @provable L Gamma (@impp L minL (@impp L minL x (@impp L minL a (@multi_imp L minL xs (@impp L minL x y)))) (@impp L minL a (@multi_imp L minL xs (@impp L minL x y)))) *)
    eapply aux_minimun_rule02; [| eauto].
(* Goal: @provable L Gamma (@impp L minL (@impp L minL a (@impp L minL x (@multi_imp L minL xs y))) (@impp L minL x (@impp L minL a (@multi_imp L minL xs y)))) *)
    apply provable_impp_arg_switch.
Qed.

Lemma provable_multi_imp_arg_switch1: forall (xs: list expr) (x y: expr), |-- (x --> multi_imp xs  y) --> multi_imp xs (x --> y).
Proof.
(* Goal: forall (G : Prop) (l : list (@sig Prop (fun X : Prop => X))), iff (forall (_ : FiniteWitnessedSequentCalculus L (@Build_SequentCalculus L (@derivable L Gamma))) (_ : @NormalAxiomatization L minL (@Build_SequentCalculus L (@derivable L Gamma))) (_ : Typeclass_Rewrite l), G) (forall _ : Typeclass_Rewrite (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (FiniteWitnessedSequentCalculus L Gamma) fwSC) l), G) *)
  intros.
(* Goal: @provable L Gamma (@impp L minL (@multi_imp L minL xs x) (@multi_imp L minL xs y)) *)
  induction xs.
  + simpl.
(* Goal: @provable L Gamma (@impp L minL x x) *)
    apply provable_impp_refl.
  + simpl.
(* Goal: @provable L Gamma (@impp L minL (@impp L minL a (@multi_imp L minL xs (@impp L minL x y))) (@impp L minL x (@impp L minL a (@multi_imp L minL xs y)))) *)
    apply aux_minimun_rule02 with (a --> x --> multi_imp xs y).
(* Goal: @provable L Gamma (@impp L minL (@impp L minL a (@impp L minL x (@multi_imp L minL xs y))) (@impp L minL x (@impp L minL a (@multi_imp L minL xs y)))) *)
    - apply provable_impp_arg_switch.
(* Goal: forall (a : @expr L) (_ : Phi a), Psi a *)
    - apply aux_minimun_rule01; auto.
Qed.

Lemma provable_multi_imp_arg_switch2: forall (xs: list expr) (x y: expr), |-- multi_imp xs (x --> y) --> (x --> multi_imp xs  y).
Proof.
(* Goal: forall (G : Prop) (l : list (@sig Prop (fun X : Prop => X))), iff (forall (_ : FiniteWitnessedSequentCalculus L (@Build_SequentCalculus L (@derivable L Gamma))) (_ : @NormalAxiomatization L minL (@Build_SequentCalculus L (@derivable L Gamma))) (_ : Typeclass_Rewrite l), G) (forall _ : Typeclass_Rewrite (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (FiniteWitnessedSequentCalculus L Gamma) fwSC) l), G) *)
  intros.
(* Goal: @provable L Gamma (@impp L minL (@multi_imp L minL xs x) (@multi_imp L minL xs y)) *)
  induction xs.
  + simpl.
(* Goal: @provable L Gamma (@impp L minL x x) *)
    apply provable_impp_refl.
  + simpl.
(* Goal: @provable L Gamma (@impp L minL (@impp L minL a (@multi_imp L minL xs (@impp L minL x y))) (@impp L minL x (@impp L minL a (@multi_imp L minL xs y)))) *)
    apply aux_minimun_rule02 with (a --> x --> multi_imp xs y).
(* Goal: forall (a : @expr L) (_ : Phi a), Psi a *)
    - apply aux_minimun_rule01; auto.
(* Goal: @provable L Gamma (@impp L minL (@impp L minL a (@impp L minL x (@multi_imp L minL xs y))) (@impp L minL x (@impp L minL a (@multi_imp L minL xs y)))) *)
    - apply provable_impp_arg_switch.
Qed.

Lemma provable_multi_imp_weaken: forall (xs: list expr) (x y: expr), |-- x --> y -> |-- multi_imp xs x --> multi_imp xs y.
Proof.
(* Goal: forall (G : Prop) (l : list (@sig Prop (fun X : Prop => X))), iff (forall (_ : FiniteWitnessedSequentCalculus L (@Build_SequentCalculus L (@derivable L Gamma))) (_ : @NormalAxiomatization L minL (@Build_SequentCalculus L (@derivable L Gamma))) (_ : Typeclass_Rewrite l), G) (forall _ : Typeclass_Rewrite (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (FiniteWitnessedSequentCalculus L Gamma) fwSC) l), G) *)
  intros.
(* Goal: @provable L Gamma (@impp L minL (@multi_imp L minL xs x) (@multi_imp L minL xs y)) *)
  induction xs.
(* Goal: forall (a : @expr L) (_ : Phi a), Psi a *)
  + auto.
(* Goal: forall (a : @expr L) (_ : Phi a), Psi a *)
  + apply aux_minimun_rule01; auto.
Qed.

(* TODO: maybe this one is also not useful now. *)
Lemma provable_multi_imp_split:
  forall Phi1 Phi2 (xs: list expr) (y: expr),
    Forall (Union _ Phi1 Phi2) xs ->
    |-- multi_imp xs y ->
    exists xs1 xs2,
      Forall Phi1 xs1 /\
      Forall Phi2 xs2 /\
      |-- multi_imp xs1 (multi_imp xs2 y).
Proof.
(* Goal: forall (G : Prop) (l : list (@sig Prop (fun X : Prop => X))), iff (forall (_ : FiniteWitnessedSequentCalculus L (@Build_SequentCalculus L (@derivable L Gamma))) (_ : @NormalAxiomatization L minL (@Build_SequentCalculus L (@derivable L Gamma))) (_ : Typeclass_Rewrite l), G) (forall _ : Typeclass_Rewrite (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (FiniteWitnessedSequentCalculus L Gamma) fwSC) l), G) *)
  intros.
(* Goal: @ex (list (@expr L)) (fun xs1 : list (@expr L) => @ex (list (@expr L)) (fun xs2 : list (@expr L) => and (@Forall (@expr L) Phi1 xs1) (and (@Forall (@expr L) Phi2 xs2) (@provable L Gamma (@multi_imp L minL xs1 (@multi_imp L minL xs2 y)))))) *)
  revert y H0; induction H.
  + exists nil, nil.
(* Goal: and (@Forall (@expr L) Phi1 (@nil (@expr L))) (and (@Forall (@expr L) Phi2 (@nil (@expr L))) (@provable L Gamma (@multi_imp L minL (@nil (@expr L)) (@multi_imp L minL (@nil (@expr L)) y)))) *)
    split; [| split]; [constructor .. | auto].
(* Goal: forall (G : Prop) (l : list (@sig Prop (fun X : Prop => X))), iff (forall (_ : FiniteWitnessedSequentCalculus L (@Build_SequentCalculus L (@derivable L Gamma))) (_ : @NormalAxiomatization L minL (@Build_SequentCalculus L (@derivable L Gamma))) (_ : Typeclass_Rewrite l), G) (forall _ : Typeclass_Rewrite (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (FiniteWitnessedSequentCalculus L Gamma) fwSC) l), G) *)
  + intros.
    specialize (IHForall (x --> y)).
    eapply modus_ponens in H1;
      [| simpl; apply provable_multi_imp_arg_switch1].
(* Goal: @ex (list (@expr L)) (fun xs1 : list (@expr L) => @ex (list (@expr L)) (fun xs2 : list (@expr L) => and (@Forall (@expr L) Phi1 xs1) (and (@Forall (@expr L) Phi2 xs2) (@provable L Gamma (@multi_imp L minL xs1 (@multi_imp L minL xs2 y)))))) *)
    specialize (IHForall H1); clear H1.
(* Goal: @ex (list (@expr L)) (fun xs1 : list (@expr L) => @ex (list (@expr L)) (fun xs2 : list (@expr L) => and (@Forall (@expr L) Phi1 xs1) (and (@Forall (@expr L) Phi2 xs2) (@provable L Gamma (@multi_imp L minL xs1 (@multi_imp L minL xs2 y)))))) *)
    destruct IHForall as [xs1 [xs2 [? [? ?]]]].
(* Goal: @ex (list (@expr L)) (fun xs1 : list (@expr L) => @ex (list (@expr L)) (fun xs2 : list (@expr L) => and (@Forall (@expr L) Phi1 xs1) (and (@Forall (@expr L) Phi2 xs2) (@provable L Gamma (@multi_imp L minL xs1 (@multi_imp L minL xs2 y)))))) *)
    destruct H.
    - exists (x :: xs1), xs2.
(* Goal: forall (a : @expr L) (_ : Phi a), Psi a *)
      split; [constructor | split]; auto.
(* Goal: @provable L Gamma (@multi_imp L minL (@cons (@expr L) x xs1) (@multi_imp L minL xs2 y)) *)
      simpl; eapply modus_ponens; [apply provable_multi_imp_arg_switch2 |].
(* Goal: @provable L Gamma (@multi_imp L minL xs1 (@multi_imp L minL (@cons (@expr L) x xs2) y)) *)
      eapply modus_ponens; [apply provable_multi_imp_weaken | exact H3].
(* Goal: @provable L Gamma (@impp L minL (@multi_imp L minL xs2 (@impp L minL x y)) (@impp L minL x (@multi_imp L minL xs2 y))) *)
      apply provable_multi_imp_arg_switch2.
    - exists xs1, (x :: xs2).
(* Goal: forall (a : @expr L) (_ : Phi a), Psi a *)
      split; [| split; [constructor | ]]; auto.
(* Goal: @provable L Gamma (@multi_imp L minL xs1 (@multi_imp L minL (@cons (@expr L) x xs2) y)) *)
      eapply modus_ponens; [apply provable_multi_imp_weaken | exact H3].
(* Goal: @provable L Gamma (@impp L minL (@multi_imp L minL xs2 (@impp L minL x y)) (@impp L minL x (@multi_imp L minL xs2 y))) *)
      simpl; apply provable_multi_imp_arg_switch2.
Qed.

Lemma provable_add_multi_imp_left_head: forall xs1 xs2 y, |-- multi_imp xs2 y --> multi_imp (xs1 ++ xs2) y.
Proof.
(* Goal: forall (G : Prop) (l : list (@sig Prop (fun X : Prop => X))), iff (forall (_ : FiniteWitnessedSequentCalculus L (@Build_SequentCalculus L (@derivable L Gamma))) (_ : @NormalAxiomatization L minL (@Build_SequentCalculus L (@derivable L Gamma))) (_ : Typeclass_Rewrite l), G) (forall _ : Typeclass_Rewrite (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (FiniteWitnessedSequentCalculus L Gamma) fwSC) l), G) *)
  intros.
(* Goal: @provable L Gamma (@impp L minL (@multi_imp L minL xs2 y) (@multi_imp L minL (@app (@expr L) xs1 xs2) y)) *)
  induction xs1.
  + apply provable_impp_refl.
(* Goal: forall (a : @expr L) (_ : Phi a), Psi a *)
  + eapply aux_minimun_rule02; eauto.
(* Goal: @provable L Gamma (@impp L minL (@multi_imp L minL (@nil (@expr L)) y) (@impp L minL x y)) *)
    apply axiom1.
Qed.

Lemma provable_add_multi_imp_left_tail: forall xs1 xs2 y, |-- multi_imp xs1 y --> multi_imp (xs1 ++ xs2) y.
Proof.
(* Goal: forall (G : Prop) (l : list (@sig Prop (fun X : Prop => X))), iff (forall (_ : FiniteWitnessedSequentCalculus L (@Build_SequentCalculus L (@derivable L Gamma))) (_ : @NormalAxiomatization L minL (@Build_SequentCalculus L (@derivable L Gamma))) (_ : Typeclass_Rewrite l), G) (forall _ : Typeclass_Rewrite (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (FiniteWitnessedSequentCalculus L Gamma) fwSC) l), G) *)
  intros.
(* Goal: iff (@derivable L Gamma (Union (@expr L) Phi (fun x : @expr L => @In (@expr L) x (@cons (@expr L) a xs))) y) (@derivable L Gamma Phi (@multi_imp L minL (@cons (@expr L) a xs) y)) *)
  induction xs1; simpl.
  + pose proof (provable_add_multi_imp_left_head xs2 nil y).
(* Goal: forall (a : @expr L) (_ : Phi a), Psi a *)
    rewrite app_nil_r in H; auto.
(* Goal: forall (a : @expr L) (_ : Phi a), Psi a *)
  + apply aux_minimun_rule01; auto.
Qed.

Lemma provable_multi_imp_modus_ponens: forall xs y z, |-- multi_imp xs y --> multi_imp xs (y --> z) --> multi_imp xs z.
Proof.
(* Goal: forall (G : Prop) (l : list (@sig Prop (fun X : Prop => X))), iff (forall (_ : FiniteWitnessedSequentCalculus L (@Build_SequentCalculus L (@derivable L Gamma))) (_ : @NormalAxiomatization L minL (@Build_SequentCalculus L (@derivable L Gamma))) (_ : Typeclass_Rewrite l), G) (forall _ : Typeclass_Rewrite (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (FiniteWitnessedSequentCalculus L Gamma) fwSC) l), G) *)
  intros.
(* Goal: iff (@derivable L Gamma (Union (@expr L) Phi (fun x : @expr L => @In (@expr L) x (@cons (@expr L) a xs))) y) (@derivable L Gamma Phi (@multi_imp L minL (@cons (@expr L) a xs) y)) *)
  induction xs; simpl.
  + apply aux_minimun_theorem02.
  + eapply aux_minimun_rule02; [| apply provable_impp_arg_switch].
(* Goal: @provable L Gamma (@impp L minL (@impp L minL a (@multi_imp L minL xs y)) (@impp L minL a (@impp L minL (@impp L minL a (@multi_imp L minL xs (@impp L minL y z))) (@multi_imp L minL xs z)))) *)
    eapply aux_minimun_rule02; [| apply aux_minimun_theorem04].
(* Goal: @provable L Gamma (@impp L minL (@impp L minL a (@multi_imp L minL xs y)) (@impp L minL a (@impp L minL a (@impp L minL (@impp L minL a (@multi_imp L minL xs (@impp L minL y z))) (@multi_imp L minL xs z))))) *)
    apply aux_minimun_rule01.
(* Goal: @provable L Gamma (@impp L minL (@multi_imp L minL xs y) (@impp L minL a (@impp L minL (@impp L minL a (@multi_imp L minL xs (@impp L minL y z))) (@multi_imp L minL xs z)))) *)
    eapply aux_minimun_rule02; [eauto |].
(* Goal: @provable L Gamma (@impp L minL (@impp L minL (@multi_imp L minL xs (@impp L minL y z)) (@multi_imp L minL xs z)) (@impp L minL a (@impp L minL (@impp L minL a (@multi_imp L minL xs (@impp L minL y z))) (@multi_imp L minL xs z)))) *)
    eapply aux_minimun_rule02; [| apply provable_impp_arg_switch].
(* Goal: @provable L Gamma (@impp L minL (@impp L minL (@multi_imp L minL xs (@impp L minL y z)) (@multi_imp L minL xs z)) (@impp L minL (@impp L minL a (@multi_imp L minL xs (@impp L minL y z))) (@impp L minL a (@multi_imp L minL xs z)))) *)
    apply aux_minimun_theorem00.
Qed.

End DerivableRules_multi_impp.

Section Axiomatization2SequentCalculus.

(* Goal: DeductionWeaken L Gamma *)
(* Goal: BasicSequentCalculus L Gamma *)
Context {L: Language}
(* Goal: DeductionWeaken L Gamma *)
(* Goal: BasicSequentCalculus L Gamma *)
        {minL: MinimunLanguage L}
(* Goal: DeductionWeaken L Gamma *)
(* Goal: BasicSequentCalculus L Gamma *)
        {Gamma: ProofTheory L}
(* Goal: DeductionWeaken L Gamma *)
(* Goal: BasicSequentCalculus L Gamma *)
        {AX: NormalAxiomatization L Gamma}.

Lemma Axiomatization2SequentCalculus_SC: NormalSequentCalculus L Gamma.
Proof.
(* Goal: @MinimunAxiomatization L minL Gamma *)
  constructor.
(* Goal: forall (G : Prop) (l : list (@sig Prop (fun X : Prop => X))), iff (forall (_ : FiniteWitnessedSequentCalculus L (@Build_SequentCalculus L (@derivable L Gamma))) (_ : @NormalAxiomatization L minL (@Build_SequentCalculus L (@derivable L Gamma))) (_ : Typeclass_Rewrite l), G) (forall _ : Typeclass_Rewrite (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (FiniteWitnessedSequentCalculus L Gamma) fwSC) l), G) *)
  intros.
(* Goal: @derivable L Gamma Phi x *)
  rewrite derivable_provable.
(* Goal: forall (G : Prop) (l : list (@sig Prop (fun X : Prop => X))), iff (forall (_ : FiniteWitnessedSequentCalculus L (@Build_SequentCalculus L (@derivable L Gamma))) (_ : @NormalAxiomatization L minL (@Build_SequentCalculus L (@derivable L Gamma))) (_ : Typeclass_Rewrite l), G) (forall _ : Typeclass_Rewrite (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (FiniteWitnessedSequentCalculus L Gamma) fwSC) l), G) *)
  split; intros.
(* Goal: forall (a : @expr L) (_ : Phi a), Psi a *)
  + exists nil; split; auto.
  + destruct H as [xs [? ?]].
(* Goal: @provable L Gamma x *)
    destruct xs; [auto |].
(* Goal: @provable L Gamma x *)
    inversion H; subst.
(* Goal: @provable L Gamma x *)
    inversion H3.
Qed.

Context {minAX: MinimunAxiomatization L Gamma}.

Lemma Axiomatization2SequentCalculus_fwSC: FiniteWitnessedSequentCalculus L Gamma.
Proof.
(* Goal: @MinimunAxiomatization L minL Gamma *)
  constructor.
(* Goal: forall (G : Prop) (l : list (@sig Prop (fun X : Prop => X))), iff (forall (_ : FiniteWitnessedSequentCalculus L (@Build_SequentCalculus L (@derivable L Gamma))) (_ : @NormalAxiomatization L minL (@Build_SequentCalculus L (@derivable L Gamma))) (_ : Typeclass_Rewrite l), G) (forall _ : Typeclass_Rewrite (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (FiniteWitnessedSequentCalculus L Gamma) fwSC) l), G) *)
  hnf; intros.
(* Goal: @ex (list (@expr L)) (fun xs : list (@expr L) => and (@Forall (@expr L) Phi xs) (@derivable L Gamma (fun x : @expr L => @In (@expr L) x xs) y)) *)
  rewrite derivable_provable in H.
(* Goal: @derivable L Gamma Phi y *)
  destruct H as [xs [? ?]].
(* Goal: @ex (list (@expr L)) (fun xs0 : list (@expr L) => and (@Forall (@expr L) (fun x : @expr L => @In (@expr L) x xs) xs0) (@provable L Gamma (@multi_imp L minL xs0 y))) *)
  exists xs.
(* Goal: forall (a : @expr L) (_ : Phi a), Psi a *)
  split; auto.
(* Goal: @derivable L Gamma Phi x *)
  rewrite derivable_provable.
(* Goal: @ex (list (@expr L)) (fun xs0 : list (@expr L) => and (@Forall (@expr L) (fun x : @expr L => @In (@expr L) x xs) xs0) (@provable L Gamma (@multi_imp L minL xs0 y))) *)
  exists xs.
(* Goal: forall (a : @expr L) (_ : Phi a), Psi a *)
  split; auto.
(* Goal: forall (a : @expr L) (_ : Phi a), Psi a *)
  rewrite Forall_forall; auto.
Qed.

Lemma Axiomatization2SequentCalculus_minSC: MinimunSequentCalculus L Gamma.
Proof.
(* Goal: @MinimunAxiomatization L minL Gamma *)
  constructor.
(* Goal: forall (G : Prop) (l : list (@sig Prop (fun X : Prop => X))), iff (forall (_ : FiniteWitnessedSequentCalculus L (@Build_SequentCalculus L (@derivable L Gamma))) (_ : @NormalAxiomatization L minL (@Build_SequentCalculus L (@derivable L Gamma))) (_ : Typeclass_Rewrite l), G) (forall _ : Typeclass_Rewrite (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (FiniteWitnessedSequentCalculus L Gamma) fwSC) l), G) *)
  + intros.
    rewrite derivable_provable in H, H0 |- *.
(* Goal: @ex (list (@expr L)) (fun xs : list (@expr L) => and (@Forall (@expr L) (fun x : @expr L => Phi x) xs) (@provable L Gamma (@multi_imp L minL xs y))) *)
    destruct H as [xs1 [? ?]], H0 as [xs2 [? ?]].
    exists (xs1 ++ xs2); split.
(* Goal: forall (a : @expr L) (_ : Phi a), Psi a *)
    - rewrite Forall_app_iff; auto.
    - pose proof modus_ponens _ _ (provable_add_multi_imp_left_tail xs1 xs2 _) H1.
(* Goal: @provable L Gamma (@multi_imp L minL (@app (@expr L) xs1 xs2) y) *)
      pose proof modus_ponens _ _ (provable_add_multi_imp_left_head xs1 xs2 _) H2.
      pose proof provable_multi_imp_modus_ponens (xs1 ++ xs2) x y.
(* Goal: @provable L Gamma (@multi_imp L minL (@app (@expr L) xs1 xs2) y) *)
      pose proof modus_ponens _ _ H5 H3.
(* Goal: @provable L Gamma (@multi_imp L minL (@app (@expr L) xs1 xs2) y) *)
      pose proof modus_ponens _ _ H6 H4.
(* Goal: forall (a : @expr L) (_ : Phi a), Psi a *)
      auto.
(* Goal: forall (G : Prop) (l : list (@sig Prop (fun X : Prop => X))), iff (forall (_ : FiniteWitnessedSequentCalculus L (@Build_SequentCalculus L (@derivable L Gamma))) (_ : @NormalAxiomatization L minL (@Build_SequentCalculus L (@derivable L Gamma))) (_ : Typeclass_Rewrite l), G) (forall _ : Typeclass_Rewrite (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (FiniteWitnessedSequentCalculus L Gamma) fwSC) l), G) *)
  + intros.
    rewrite derivable_provable in H |- *.
(* Goal: @derivable L Gamma Phi y *)
    destruct H as [xs [? ?]].
(* Goal: @ex (list (@expr L)) (fun xs : list (@expr L) => and (@Forall (@expr L) (fun x : @expr L => Phi x) xs) (@provable L Gamma (@multi_imp L minL xs (@impp L minL x y)))) *)
    pose proof provable_multi_imp_split _ _ _ _ H H0 as [xs1 [xs2 [? [? ?]]]].
(* Goal: @ex (list (@expr L)) (fun xs : list (@expr L) => and (@Forall (@expr L) (fun x : @expr L => Phi x) xs) (@provable L Gamma (@multi_imp L minL xs (@impp L minL x y)))) *)
    exists xs1.
(* Goal: forall (a : @expr L) (_ : Phi a), Psi a *)
    split; auto.
(* Goal: @provable L Gamma (@multi_imp L minL xs1 (@impp L minL x y)) *)
    eapply modus_ponens; [| exact H3].
(* Goal: @provable L Gamma (@impp L minL (@multi_imp L minL xs1 (@multi_imp L minL xs2 y)) (@multi_imp L minL xs1 (@impp L minL x y))) *)
    apply provable_multi_imp_weaken.
    clear - H2 minAX.
(* Goal: @provable L Gamma (@impp L minL (@multi_imp L minL xs2 y) (@impp L minL x y)) *)
    induction H2.
(* Goal: @provable L Gamma (@impp L minL (@multi_imp L minL (@nil (@expr L)) y) (@impp L minL x y)) *)
    - apply axiom1.
(* Goal: @provable L Gamma (@impp L minL (@impp L minL y z) (@impp L minL (@impp L minL x y) (@impp L minL x z))) *)
    - inversion H; subst x0; clear H.
(* Goal: iff (@derivable L Gamma (Union (@expr L) Phi (fun x : @expr L => @In (@expr L) x (@cons (@expr L) a xs))) y) (@derivable L Gamma Phi (@multi_imp L minL (@cons (@expr L) a xs) y)) *)
      simpl.
(* Goal: @provable L Gamma (@impp L minL (@impp L minL x (@multi_imp L minL l y)) (@impp L minL x y)) *)
      pose proof aux_minimun_theorem04 x y.
(* Goal: @provable L Gamma (@impp L minL (@impp L minL x (@multi_imp L minL l y)) (@impp L minL x y)) *)
      pose proof aux_minimun_rule01 _ _ x IHForall.
(* Goal: @provable L Gamma (@impp L minL (@impp L minL x (@multi_imp L minL l y)) (@impp L minL x y)) *)
      eapply aux_minimun_rule02; [exact H0 | exact H].
Qed.

Lemma Axiomatization2SequentCalculus_bSC: BasicSequentCalculus L Gamma.
Proof.
(* Goal: BasicSequentCalculus L Gamma *)
  assert (DW: DeductionWeaken L Gamma).
(* Goal: DeductionWeaken L Gamma *)
(* Goal: BasicSequentCalculus L Gamma *)
  {
(* Goal: forall (G : Prop) (l : list (@sig Prop (fun X : Prop => X))), iff (forall (_ : FiniteWitnessedSequentCalculus L (@Build_SequentCalculus L (@derivable L Gamma))) (_ : @NormalAxiomatization L minL (@Build_SequentCalculus L (@derivable L Gamma))) (_ : Typeclass_Rewrite l), G) (forall _ : Typeclass_Rewrite (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (FiniteWitnessedSequentCalculus L Gamma) fwSC) l), G) *)
    hnf; intros.
    rewrite derivable_provable in H0 |- *.
(* Goal: @ex (list (@expr L)) (fun xs : list (@expr L) => and (@Forall (@expr L) (fun x : @expr L => Psi x) xs) (@provable L Gamma (@multi_imp L minL xs x))) *)
    destruct H0 as [xs [? ?]].
(* Goal: forall (a : @expr L) (_ : Phi a), Psi a *)
    exists xs; split; auto.
(* Goal: @Forall (@expr L) (fun x : @expr L => Psi x) xs *)
    revert H0; apply Forall_impl.
(* Goal: forall (a : @expr L) (_ : Phi a), Psi a *)
    auto.
  }
(* Goal: forall (a : @expr L) (_ : Phi a), Psi a *)
  constructor; auto.
(* Goal: forall (G : Prop) (l : list (@sig Prop (fun X : Prop => X))), iff (forall (_ : FiniteWitnessedSequentCalculus L (@Build_SequentCalculus L (@derivable L Gamma))) (_ : @NormalAxiomatization L minL (@Build_SequentCalculus L (@derivable L Gamma))) (_ : Typeclass_Rewrite l), G) (forall _ : Typeclass_Rewrite (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (FiniteWitnessedSequentCalculus L Gamma) fwSC) l), G) *)
  + intros.
(* Goal: @derivable L Gamma Phi x *)
    rewrite derivable_provable.
(* Goal: @ex (list (@expr L)) (fun xs : list (@expr L) => and (@Forall (@expr L) (fun x : @expr L => Phi x) xs) (@provable L Gamma (@multi_imp L minL xs x))) *)
    exists (x :: nil); split.
(* Goal: forall (a : @expr L) (_ : Phi a), Psi a *)
    - constructor; auto.
(* Goal: iff (@derivable L Gamma (Union (@expr L) Phi (fun x : @expr L => @In (@expr L) x (@cons (@expr L) a xs))) y) (@derivable L Gamma Phi (@multi_imp L minL (@cons (@expr L) a xs) y)) *)
    - simpl.
(* Goal: @provable L Gamma (@impp L minL x x) *)
      apply provable_impp_refl.
  + apply DeductionWeaken_ContextualDerivableFiniteWitnessed_DeductionSubst1_2_DeductionSubst.
    - exact DW.
    - apply DeductionWeaken_DerivableFiniteWitnessed_2_ContextualDerivableFiniteWitnessed.
(* Goal: DeductionWeaken L Gamma *)
      * exact DW.
      * exact (@derivable_finite_witnessed _ _ Axiomatization2SequentCalculus_fwSC).
    - apply DeductionImpIntro_DeductionMP_2_DeductionSubst1.
      * exact (@deduction_impp_intros _ _ _ Axiomatization2SequentCalculus_minSC).
      * exact (@deduction_modus_ponens _ _ _ Axiomatization2SequentCalculus_minSC).
Qed.

End Axiomatization2SequentCalculus.

Section DerivableRulesFromSequentCalculus.

(* Goal: DeductionWeaken L Gamma *)
(* Goal: BasicSequentCalculus L Gamma *)
Context {L: Language}
(* Goal: DeductionWeaken L Gamma *)
(* Goal: BasicSequentCalculus L Gamma *)
        {Gamma: ProofTheory L}
(* Goal: DeductionWeaken L Gamma *)
(* Goal: BasicSequentCalculus L Gamma *)
        {bSC: BasicSequentCalculus L Gamma}.

(* Goal: DeductionWeaken L Gamma *)
(* Goal: BasicSequentCalculus L Gamma *)
Context {minL: MinimunLanguage L}
(* Goal: DeductionWeaken L Gamma *)
(* Goal: BasicSequentCalculus L Gamma *)
        {minSC: MinimunSequentCalculus L Gamma}.

Lemma deduction_impp_elim: forall Phi x y,
  Phi |-- impp x y ->
  Union _ Phi (Singleton _ x) |-- y.
Proof.
(* Goal: forall (G : Prop) (l : list (@sig Prop (fun X : Prop => X))), iff (forall (_ : FiniteWitnessedSequentCalculus L (@Build_SequentCalculus L (@derivable L Gamma))) (_ : @NormalAxiomatization L minL (@Build_SequentCalculus L (@derivable L Gamma))) (_ : Typeclass_Rewrite l), G) (forall _ : Typeclass_Rewrite (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (FiniteWitnessedSequentCalculus L Gamma) fwSC) l), G) *)
  intros.
(* Goal: @derivable L Gamma (Union (@expr L) Phi (Singleton (@expr L) x)) y *)
  eapply deduction_modus_ponens; solve_assum.
Qed.

Theorem deduction_theorem:
  forall (Phi: context) (x y: expr),
    Union _ Phi (Singleton _ x) |-- y <->
    Phi |-- x --> y.
Proof.
(* Goal: forall (Phi : @context L) (x y : @expr L), iff (@derivable L Gamma (Union (@expr L) Phi (Singleton (@expr L) x)) y) (@derivable L Gamma Phi (@impp L minL x y)) *)
  intros; split.
(* Goal: forall (a : @expr L) (_ : Phi a), Psi a *)
  + apply deduction_impp_intros; auto.
(* Goal: forall (a : @expr L) (_ : Phi a), Psi a *)
  + apply deduction_impp_elim; auto.
Qed.

Theorem deduction_theorem_multi_imp:
  forall (Phi: context) (xs: list expr) (y: expr),
    Union _ Phi (fun x => In x xs) |-- y <->
    Phi |-- multi_imp xs y.
Proof.
(* Goal: forall (G : Prop) (l : list (@sig Prop (fun X : Prop => X))), iff (forall (_ : FiniteWitnessedSequentCalculus L (@Build_SequentCalculus L (@derivable L Gamma))) (_ : @NormalAxiomatization L minL (@Build_SequentCalculus L (@derivable L Gamma))) (_ : Typeclass_Rewrite l), G) (forall _ : Typeclass_Rewrite (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (FiniteWitnessedSequentCalculus L Gamma) fwSC) l), G) *)
  intros.
(* Goal: forall (G : Prop) (l : list (@sig Prop (fun X : Prop => X))), iff (forall (_ : FiniteWitnessedSequentCalculus L (@Build_SequentCalculus L (@derivable L Gamma))) (_ : @NormalAxiomatization L minL (@Build_SequentCalculus L (@derivable L Gamma))) (_ : Typeclass_Rewrite l), G) (forall _ : Typeclass_Rewrite (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (FiniteWitnessedSequentCalculus L Gamma) fwSC) l), G) *)
  revert Phi; induction xs; intros.
  + simpl.
    split; apply deduction_weaken;
(* Goal: forall (G : Prop) (l : list (@sig Prop (fun X : Prop => X))), iff (forall (_ : FiniteWitnessedSequentCalculus L (@Build_SequentCalculus L (@derivable L Gamma))) (_ : @NormalAxiomatization L minL (@Build_SequentCalculus L (@derivable L Gamma))) (_ : Typeclass_Rewrite l), G) (forall _ : Typeclass_Rewrite (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (FiniteWitnessedSequentCalculus L Gamma) fwSC) l), G) *)
    unfold Included, Ensembles.In; intros.
    - rewrite Union_spec in H.
(* Goal: forall (a : @expr L) (_ : Phi a), Psi a *)
      tauto.
    - rewrite Union_spec.
(* Goal: forall (a : @expr L) (_ : Phi a), Psi a *)
      tauto.
  + simpl.
    rewrite <- deduction_theorem, <- IHxs.
    split; apply deduction_weaken;
(* Goal: forall (G : Prop) (l : list (@sig Prop (fun X : Prop => X))), iff (forall (_ : FiniteWitnessedSequentCalculus L (@Build_SequentCalculus L (@derivable L Gamma))) (_ : @NormalAxiomatization L minL (@Build_SequentCalculus L (@derivable L Gamma))) (_ : Typeclass_Rewrite l), G) (forall _ : Typeclass_Rewrite (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (FiniteWitnessedSequentCalculus L Gamma) fwSC) l), G) *)
    unfold Included, Ensembles.In; intros.
    - rewrite Union_spec in H.
(* Goal: Union (@expr L) (Union (@expr L) Phi (Singleton (@expr L) a)) (fun x : @expr L => @In (@expr L) x xs) x *)
      rewrite !Union_spec, Singleton_spec.
(* Goal: forall (a : @expr L) (_ : Phi a), Psi a *)
      tauto.
    - rewrite !Union_spec, Singleton_spec in H.
(* Goal: Union (@expr L) Phi (fun x : @expr L => or (@eq (@expr L) a x) (@In (@expr L) x xs)) x *)
      rewrite !Union_spec.
(* Goal: forall (a : @expr L) (_ : Phi a), Psi a *)
      tauto.
Qed.

Lemma derivable_impp_refl: forall (Phi: context) (x: expr), Phi |-- x --> x.
Proof.
(* Goal: forall (G : Prop) (l : list (@sig Prop (fun X : Prop => X))), iff (forall (_ : FiniteWitnessedSequentCalculus L (@Build_SequentCalculus L (@derivable L Gamma))) (_ : @NormalAxiomatization L minL (@Build_SequentCalculus L (@derivable L Gamma))) (_ : Typeclass_Rewrite l), G) (forall _ : Typeclass_Rewrite (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (FiniteWitnessedSequentCalculus L Gamma) fwSC) l), G) *)
  intros.
(* Goal: @derivable L Gamma Phi (@impp L minL y x) *)
  apply deduction_theorem.
(* Goal: @derivable L Gamma (Union (@expr L) (Union (@expr L) Phi (Singleton (@expr L) x)) (Singleton (@expr L) y)) x *)
  solve_assum.
Qed.

Lemma deduction_left_impp_intros: forall (Phi: context) (x y: expr),
  Phi |-- x ->
  Phi |-- y --> x.
Proof.
(* Goal: forall (G : Prop) (l : list (@sig Prop (fun X : Prop => X))), iff (forall (_ : FiniteWitnessedSequentCalculus L (@Build_SequentCalculus L (@derivable L Gamma))) (_ : @NormalAxiomatization L minL (@Build_SequentCalculus L (@derivable L Gamma))) (_ : Typeclass_Rewrite l), G) (forall _ : Typeclass_Rewrite (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (FiniteWitnessedSequentCalculus L Gamma) fwSC) l), G) *)
  intros.
(* Goal: @derivable L Gamma Phi (@impp L minL y x) *)
  apply deduction_theorem.
(* Goal: @derivable L Gamma (Union (@expr L) (Union (@expr L) Phi (Singleton (@expr L) x)) (Singleton (@expr L) y)) x *)
  solve_assum.
Qed.

Lemma derivable_axiom1: forall (Phi: context) (x y: expr),
  Phi |-- x --> y --> x.
Proof.
(* Goal: forall (G : Prop) (l : list (@sig Prop (fun X : Prop => X))), iff (forall (_ : FiniteWitnessedSequentCalculus L (@Build_SequentCalculus L (@derivable L Gamma))) (_ : @NormalAxiomatization L minL (@Build_SequentCalculus L (@derivable L Gamma))) (_ : Typeclass_Rewrite l), G) (forall _ : Typeclass_Rewrite (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (FiniteWitnessedSequentCalculus L Gamma) fwSC) l), G) *)
  intros.
  rewrite <- !deduction_theorem.
(* Goal: @derivable L Gamma (Union (@expr L) (Union (@expr L) Phi (Singleton (@expr L) x)) (Singleton (@expr L) y)) x *)
  solve_assum.
Qed.

Lemma derivable_axiom2: forall (Phi: context) (x y z: expr),
  Phi |-- (x --> y --> z) --> (x --> y) --> (x --> z).
Proof.
(* Goal: forall (G : Prop) (l : list (@sig Prop (fun X : Prop => X))), iff (forall (_ : FiniteWitnessedSequentCalculus L (@Build_SequentCalculus L (@derivable L Gamma))) (_ : @NormalAxiomatization L minL (@Build_SequentCalculus L (@derivable L Gamma))) (_ : Typeclass_Rewrite l), G) (forall _ : Typeclass_Rewrite (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (FiniteWitnessedSequentCalculus L Gamma) fwSC) l), G) *)
  intros.
  rewrite <- !deduction_theorem.
(* Goal: @derivable L Gamma (Union (@expr L) (Union (@expr L) (Union (@expr L) Phi (Singleton (@expr L) (@impp L minL x (@impp L minL y z)))) (Singleton (@expr L) (@impp L minL x y))) (Singleton (@expr L) x)) z *)
  apply deduction_modus_ponens with y.
  + apply deduction_modus_ponens with x; solve_assum.
  + apply deduction_modus_ponens with x; solve_assum.
Qed.

Lemma derivable_modus_ponens: forall (Phi: context) (x y: expr),
  Phi |-- x --> (x --> y) --> y.
Proof.
(* Goal: forall (G : Prop) (l : list (@sig Prop (fun X : Prop => X))), iff (forall (_ : FiniteWitnessedSequentCalculus L (@Build_SequentCalculus L (@derivable L Gamma))) (_ : @NormalAxiomatization L minL (@Build_SequentCalculus L (@derivable L Gamma))) (_ : Typeclass_Rewrite l), G) (forall _ : Typeclass_Rewrite (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (FiniteWitnessedSequentCalculus L Gamma) fwSC) l), G) *)
  intros.
  rewrite <- !deduction_theorem.
(* Goal: @derivable L Gamma (Union (@expr L) (Union (@expr L) Phi (Singleton (@expr L) x)) (Singleton (@expr L) y)) x *)
  apply deduction_modus_ponens with x; solve_assum.
Qed.

Lemma deduction_impp_trans: forall (Phi: context) (x y z: expr),
  Phi |-- x --> y ->
  Phi |-- y --> z ->
  Phi |-- x --> z.
Proof.
(* Goal: forall (G : Prop) (l : list (@sig Prop (fun X : Prop => X))), iff (forall (_ : FiniteWitnessedSequentCalculus L (@Build_SequentCalculus L (@derivable L Gamma))) (_ : @NormalAxiomatization L minL (@Build_SequentCalculus L (@derivable L Gamma))) (_ : Typeclass_Rewrite l), G) (forall _ : Typeclass_Rewrite (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (FiniteWitnessedSequentCalculus L Gamma) fwSC) l), G) *)
  intros.
  rewrite <- deduction_theorem in H |- *.
(* Goal: @derivable L Gamma (Union (@expr L) (Union (@expr L) Phi (Singleton (@expr L) x)) (Singleton (@expr L) y)) x *)
  apply deduction_modus_ponens with y; solve_assum.
Qed.

Lemma deduction_impp_arg_switch: forall (Phi: context) (x y z: expr),
  Phi |-- x --> y --> z ->
  Phi |-- y --> x --> z.
Proof.
(* Goal: forall (G : Prop) (l : list (@sig Prop (fun X : Prop => X))), iff (forall (_ : FiniteWitnessedSequentCalculus L (@Build_SequentCalculus L (@derivable L Gamma))) (_ : @NormalAxiomatization L minL (@Build_SequentCalculus L (@derivable L Gamma))) (_ : Typeclass_Rewrite l), G) (forall _ : Typeclass_Rewrite (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (FiniteWitnessedSequentCalculus L Gamma) fwSC) l), G) *)
  intros.
  rewrite <- !deduction_theorem in *.
(* Goal: @derivable L Gamma (Union (@expr L) (Union (@expr L) Phi (Singleton (@expr L) y)) (Singleton (@expr L) x)) z *)
  eapply deduction_weaken; [| exact H].
(* Goal: Included (@expr L) (Union (@expr L) (Union (@expr L) Phi (Singleton (@expr L) x)) (Singleton (@expr L) y)) (Union (@expr L) (Union (@expr L) Phi (Singleton (@expr L) y)) (Singleton (@expr L) x)) *)
  intros ? ?.
(* Goal: Ensembles.In (@expr L) (Union (@expr L) (Union (@expr L) Phi (Singleton (@expr L) y)) (Singleton (@expr L) x)) x0 *)
  destruct H0; [destruct H0 |].
(* Goal: forall (a : @expr L) (_ : Phi a), Psi a *)
  + left; left; auto.
(* Goal: forall (a : @expr L) (_ : Phi a), Psi a *)
  + right; auto.
(* Goal: forall (a : @expr L) (_ : Phi a), Psi a *)
  + left; right; auto.
Qed.

End DerivableRulesFromSequentCalculus.

Section SequentCalculus2Axiomatization.

(* Goal: DeductionWeaken L Gamma *)
(* Goal: BasicSequentCalculus L Gamma *)
Context {L: Language}
(* Goal: DeductionWeaken L Gamma *)
(* Goal: BasicSequentCalculus L Gamma *)
        {Gamma: ProofTheory L}
(* Goal: DeductionWeaken L Gamma *)
(* Goal: BasicSequentCalculus L Gamma *)
        {minL: MinimunLanguage L}
(* Goal: DeductionWeaken L Gamma *)
(* Goal: BasicSequentCalculus L Gamma *)
        {SC: NormalSequentCalculus L Gamma}
(* Goal: DeductionWeaken L Gamma *)
(* Goal: BasicSequentCalculus L Gamma *)
        {bSC: BasicSequentCalculus L Gamma}
(* Goal: DeductionWeaken L Gamma *)
(* Goal: BasicSequentCalculus L Gamma *)
        {minSC: MinimunSequentCalculus L Gamma}.

Theorem SequentCalculus2Axiomatization_minAX: MinimunAxiomatization L Gamma.
Proof.
(* Goal: @MinimunAxiomatization L minL Gamma *)
  constructor.
  + intros x y.
(* Goal: forall (_ : @provable L Gamma (@impp L minL x y)) (_ : @provable L Gamma x), @provable L Gamma y *)
    rewrite !provable_derivable.
(* Goal: forall (G : Prop) (l : list (@sig Prop (fun X : Prop => X))), iff (forall (_ : FiniteWitnessedSequentCalculus L (@Build_SequentCalculus L (@derivable L Gamma))) (_ : @NormalAxiomatization L minL (@Build_SequentCalculus L (@derivable L Gamma))) (_ : Typeclass_Rewrite l), G) (forall _ : Typeclass_Rewrite (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (FiniteWitnessedSequentCalculus L Gamma) fwSC) l), G) *)
    intros.
(* Goal: forall (a : @expr L) (_ : Phi a), Psi a *)
    eapply deduction_modus_ponens; eauto.
  + intros x y.
(* Goal: @provable L Gamma (@impp L minL (@impp L minL x (@impp L minL y z)) (@impp L minL (@impp L minL x y) (@impp L minL x z))) *)
    rewrite provable_derivable.
(* Goal: @derivable L Gamma (@empty_context L) (@impp L minL x (@impp L minL y x)) *)
    apply derivable_axiom1.
  + intros x y z.
(* Goal: @provable L Gamma (@impp L minL (@impp L minL x (@impp L minL y z)) (@impp L minL (@impp L minL x y) (@impp L minL x z))) *)
    rewrite provable_derivable.
(* Goal: @derivable L Gamma (@empty_context L) (@impp L minL (@impp L minL x (@impp L minL y z)) (@impp L minL (@impp L minL x y) (@impp L minL x z))) *)
    apply derivable_axiom2.
Qed.

(* Goal: DeductionWeaken L Gamma *)
(* Goal: BasicSequentCalculus L Gamma *)
Theorem SequentCalculus2Axiomatization_AX {fwSC: FiniteWitnessedSequentCalculus L Gamma}: NormalAxiomatization L Gamma.
Proof.
(* Goal: forall (G : Prop) (l : list (@sig Prop (fun X : Prop => X))), iff (forall (_ : FiniteWitnessedSequentCalculus L (@Build_SequentCalculus L (@derivable L Gamma))) (_ : @NormalAxiomatization L minL (@Build_SequentCalculus L (@derivable L Gamma))) (_ : Typeclass_Rewrite l), G) (forall _ : Typeclass_Rewrite (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (FiniteWitnessedSequentCalculus L Gamma) fwSC) l), G) *)
  constructor; intros.
(* Goal: forall (G : Prop) (l : list (@sig Prop (fun X : Prop => X))), iff (forall (_ : FiniteWitnessedSequentCalculus L (@Build_SequentCalculus L (@derivable L Gamma))) (_ : @NormalAxiomatization L minL (@Build_SequentCalculus L (@derivable L Gamma))) (_ : Typeclass_Rewrite l), G) (forall _ : Typeclass_Rewrite (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (FiniteWitnessedSequentCalculus L Gamma) fwSC) l), G) *)
  split; intros.
  + apply derivable_finite_witnessed in H.
(* Goal: @ex (list (@expr L)) (fun xs0 : list (@expr L) => and (@Forall (@expr L) (fun x : @expr L => @In (@expr L) x xs) xs0) (@provable L Gamma (@multi_imp L minL xs0 y))) *)
    destruct H as [xs [? ?]]; exists xs.
(* Goal: forall (a : @expr L) (_ : Phi a), Psi a *)
    split; auto.
(* Goal: @provable L Gamma (@multi_imp L minL xs y) *)
    apply provable_derivable.
(* Goal: @derivable L Gamma (@empty_context L) (@multi_imp L minL xs y) *)
    apply deduction_theorem_multi_imp.
(* Goal: forall (a : @expr L) (_ : Phi a), Psi a *)
    eapply deduction_weaken; eauto.
(* Goal: Included (@expr L) (fun x : @expr L => @In (@expr L) x xs) (Union (@expr L) (@empty_context L) (fun x : @expr L => @In (@expr L) x xs)) *)
    apply right_Included_Union.
  + destruct H as [xs [? ?]].
(* Goal: @derivable L Gamma Phi y *)
    apply provable_derivable in H0.
(* Goal: @derivable L Gamma Phi y *)
    apply deduction_theorem_multi_imp in H0.
(* Goal: forall (a : @expr L) (_ : Phi a), Psi a *)
    eapply deduction_weaken; eauto.
(* Goal: forall (G : Prop) (l : list (@sig Prop (fun X : Prop => X))), iff (forall (_ : FiniteWitnessedSequentCalculus L (@Build_SequentCalculus L (@derivable L Gamma))) (_ : @NormalAxiomatization L minL (@Build_SequentCalculus L (@derivable L Gamma))) (_ : Typeclass_Rewrite l), G) (forall _ : Typeclass_Rewrite (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (FiniteWitnessedSequentCalculus L Gamma) fwSC) l), G) *)
    unfold Included, Ensembles.In; intros.
(* Goal: Phi x *)
    rewrite Union_spec in H1.
(* Goal: Phi x *)
    destruct H1 as [[] |].
(* Goal: Phi x *)
    revert x H1.
(* Goal: forall (a : @expr L) (_ : Phi a), Psi a *)
    rewrite Forall_forall in H; auto.
Qed.

End SequentCalculus2Axiomatization.

Definition Build_AxiomaticProofTheory {L: Language} {minL: MinimunLanguage L} (Provable: expr -> Prop): ProofTheory L :=
  Build_ProofTheory L Provable
   (fun Phi y => exists xs, Forall (fun x => Phi x) xs /\ Provable (multi_imp xs y)).

Definition Build_AxiomaticProofTheory_AX {L: Language} {minL: MinimunLanguage L} (Provable: expr -> Prop): NormalAxiomatization L (Build_AxiomaticProofTheory Provable) :=
  Build_NormalAxiomatization L minL (Build_AxiomaticProofTheory Provable) (fun _ _ => iff_refl _).

Definition Build_SequentCalculus {L: Language} (Derivable: context -> expr -> Prop): ProofTheory L :=
  Build_ProofTheory L (fun x => Derivable (Empty_set _) x) Derivable.

Definition Build_SequentCalculus_SC {L: Language} (Derivable: context -> expr -> Prop): NormalSequentCalculus L (Build_SequentCalculus Derivable) :=
  Build_NormalSequentCalculus L (Build_SequentCalculus Derivable) (fun _ => iff_refl _).

Inductive Typeclass_Rewrite (l: list (sig (fun X: Prop => X))): Prop :=
| Typeclass_Rewrite_I : Typeclass_Rewrite l.

Definition OpaqueProp (P: Prop): Prop := P.

Ltac revert_dep_rec T :=
  match goal with
  | H: context [T] |- _ =>
      first [ revert H | revert_dep_rec H]; revert_dep_rec T
  | _ => idtac
  end.

Ltac revert_dep Gamma :=
  match goal with
  | |- ?G => change (OpaqueProp G)
  end;
  revert_dep_rec Gamma.

Lemma ready_for_intros: forall G: Prop, OpaqueProp (Typeclass_Rewrite nil -> G) -> OpaqueProp G.
Proof.
(* Goal: forall (G : Prop) (l : list (@sig Prop (fun X : Prop => X))), iff (forall (_ : FiniteWitnessedSequentCalculus L (@Build_SequentCalculus L (@derivable L Gamma))) (_ : @NormalAxiomatization L minL (@Build_SequentCalculus L (@derivable L Gamma))), OpaqueProp (OpaqueProp (forall _ : Typeclass_Rewrite l, G))) (OpaqueProp (forall _ : Typeclass_Rewrite (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (FiniteWitnessedSequentCalculus L Gamma) fwSC) l), G)) *)
  unfold OpaqueProp.
(* Goal: forall (G : Prop) (l : list (@sig Prop (fun X : Prop => X))), iff (forall (_ : FiniteWitnessedSequentCalculus L (@Build_SequentCalculus L (@derivable L Gamma))) (_ : @NormalAxiomatization L minL (@Build_SequentCalculus L (@derivable L Gamma))) (_ : Typeclass_Rewrite l), G) (forall _ : Typeclass_Rewrite (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (FiniteWitnessedSequentCalculus L Gamma) fwSC) l), G) *)
  intros.
(* Goal: G *)
  apply H.
  apply  Typeclass_Rewrite_I.
Qed.

Lemma intro_with_record: forall (l: list (sig (fun X: Prop => X))) (P: Prop) (G: P -> Prop),
  (forall _____: P, OpaqueProp (Typeclass_Rewrite ((exist (fun X: Prop => X) P _____) :: l) -> G _____)) ->
  OpaqueProp (Typeclass_Rewrite l -> forall _____: P, G _____).
Proof.
(* Goal: forall (G : Prop) (l : list (@sig Prop (fun X : Prop => X))), iff (forall (_ : FiniteWitnessedSequentCalculus L (@Build_SequentCalculus L (@derivable L Gamma))) (_ : @NormalAxiomatization L minL (@Build_SequentCalculus L (@derivable L Gamma))), OpaqueProp (OpaqueProp (forall _ : Typeclass_Rewrite l, G))) (OpaqueProp (forall _ : Typeclass_Rewrite (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (FiniteWitnessedSequentCalculus L Gamma) fwSC) l), G)) *)
  unfold OpaqueProp.
(* Goal: forall (G : Prop) (l : list (@sig Prop (fun X : Prop => X))), iff (forall (_ : FiniteWitnessedSequentCalculus L (@Build_SequentCalculus L (@derivable L Gamma))) (_ : @NormalAxiomatization L minL (@Build_SequentCalculus L (@derivable L Gamma))) (_ : Typeclass_Rewrite l), G) (forall _ : Typeclass_Rewrite (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (FiniteWitnessedSequentCalculus L Gamma) fwSC) l), G) *)
  intros.
(* Goal: G *)
  apply H.
  apply  Typeclass_Rewrite_I.
Qed.

Ltac intros_dep :=
  match goal with
  | |- ?G => change (OpaqueProp G); simple apply ready_for_intros
  end;
  repeat
    match goal with
    | |-  OpaqueProp (Typeclass_Rewrite _ -> OpaqueProp _) => fail 1
    | _ => apply intro_with_record; intro
    end.

Ltac schedule :=
  match goal with
  | |- OpaqueProp (Typeclass_Rewrite ?L -> _) => constr: (L)
  end.

Ltac tactic_rev_rec L1 L2 :=
  match L1 with
  | nil => L2
  | cons ?H ?L => tactic_rev_rec L (cons H L2)
  end.

Ltac tactic_rev L :=
  match type of L with
  | list ?T => tactic_rev_rec L constr:(@nil T)
  end.

Lemma change_schedule: forall (l l': list (sig (fun X: Prop => X))) (G: Prop),
  OpaqueProp (Typeclass_Rewrite l -> G) ->
  OpaqueProp (Typeclass_Rewrite l' -> G).
Proof.
(* Goal: forall (G : Prop) (l : list (@sig Prop (fun X : Prop => X))), iff (forall (_ : FiniteWitnessedSequentCalculus L (@Build_SequentCalculus L (@derivable L Gamma))) (_ : @NormalAxiomatization L minL (@Build_SequentCalculus L (@derivable L Gamma))), OpaqueProp (OpaqueProp (forall _ : Typeclass_Rewrite l, G))) (OpaqueProp (forall _ : Typeclass_Rewrite (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (FiniteWitnessedSequentCalculus L Gamma) fwSC) l), G)) *)
  unfold OpaqueProp.
(* Goal: forall (G : Prop) (l : list (@sig Prop (fun X : Prop => X))), iff (forall (_ : FiniteWitnessedSequentCalculus L (@Build_SequentCalculus L (@derivable L Gamma))) (_ : @NormalAxiomatization L minL (@Build_SequentCalculus L (@derivable L Gamma))) (_ : Typeclass_Rewrite l), G) (forall _ : Typeclass_Rewrite (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (FiniteWitnessedSequentCalculus L Gamma) fwSC) l), G) *)
  intros.
(* Goal: G *)
  apply H.
  apply  Typeclass_Rewrite_I.
Qed.

Lemma pop_schedule: forall (x: (sig (fun X: Prop => X))) (l: list (sig (fun X: Prop => X))) (G: Prop),
  OpaqueProp (Typeclass_Rewrite l -> G) ->
  OpaqueProp (Typeclass_Rewrite (x :: l) -> G).
Proof.
(* Goal: forall (G : Prop) (l : list (@sig Prop (fun X : Prop => X))), iff (forall (_ : FiniteWitnessedSequentCalculus L (@Build_SequentCalculus L (@derivable L Gamma))) (_ : @NormalAxiomatization L minL (@Build_SequentCalculus L (@derivable L Gamma))), OpaqueProp (OpaqueProp (forall _ : Typeclass_Rewrite l, G))) (OpaqueProp (forall _ : Typeclass_Rewrite (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (FiniteWitnessedSequentCalculus L Gamma) fwSC) l), G)) *)
  unfold OpaqueProp.
(* Goal: forall (G : Prop) (l : list (@sig Prop (fun X : Prop => X))), iff (forall (_ : FiniteWitnessedSequentCalculus L (@Build_SequentCalculus L (@derivable L Gamma))) (_ : @NormalAxiomatization L minL (@Build_SequentCalculus L (@derivable L Gamma))) (_ : Typeclass_Rewrite l), G) (forall _ : Typeclass_Rewrite (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (FiniteWitnessedSequentCalculus L Gamma) fwSC) l), G) *)
  intros.
(* Goal: G *)
  apply H.
  apply  Typeclass_Rewrite_I.
Qed.

Lemma push_schedule: forall (x: (sig (fun X: Prop => X))) (l: list (sig (fun X: Prop => X))) (G: Prop),
  OpaqueProp (Typeclass_Rewrite (x :: l) -> G) ->
  OpaqueProp (Typeclass_Rewrite l -> G).
Proof.
(* Goal: forall (G : Prop) (l : list (@sig Prop (fun X : Prop => X))), iff (forall (_ : FiniteWitnessedSequentCalculus L (@Build_SequentCalculus L (@derivable L Gamma))) (_ : @NormalAxiomatization L minL (@Build_SequentCalculus L (@derivable L Gamma))), OpaqueProp (OpaqueProp (forall _ : Typeclass_Rewrite l, G))) (OpaqueProp (forall _ : Typeclass_Rewrite (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (FiniteWitnessedSequentCalculus L Gamma) fwSC) l), G)) *)
  unfold OpaqueProp.
(* Goal: forall (G : Prop) (l : list (@sig Prop (fun X : Prop => X))), iff (forall (_ : FiniteWitnessedSequentCalculus L (@Build_SequentCalculus L (@derivable L Gamma))) (_ : @NormalAxiomatization L minL (@Build_SequentCalculus L (@derivable L Gamma))) (_ : Typeclass_Rewrite l), G) (forall _ : Typeclass_Rewrite (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (FiniteWitnessedSequentCalculus L Gamma) fwSC) l), G) *)
  intros.
(* Goal: G *)
  apply H.
  apply  Typeclass_Rewrite_I.
Qed.

Ltac AddSC_enrich :=
  progress autorewrite with AddSC; intros; unfold OpaqueProp at 1.

Ltac AddAX_enrich :=
  progress autorewrite with AddAX; intros; unfold OpaqueProp at 1.

Lemma finish_enrich: forall (G: Prop), G -> OpaqueProp (Typeclass_Rewrite nil -> OpaqueProp G).
Proof.
(* Goal: forall (G : Prop) (l : list (@sig Prop (fun X : Prop => X))), iff (forall (_ : FiniteWitnessedSequentCalculus L (@Build_SequentCalculus L (@derivable L Gamma))) (_ : @NormalAxiomatization L minL (@Build_SequentCalculus L (@derivable L Gamma))), OpaqueProp (OpaqueProp (forall _ : Typeclass_Rewrite l, G))) (OpaqueProp (forall _ : Typeclass_Rewrite (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (FiniteWitnessedSequentCalculus L Gamma) fwSC) l), G)) *)
  unfold OpaqueProp.
(* Goal: forall (G : Prop) (l : list (@sig Prop (fun X : Prop => X))), iff (forall (_ : FiniteWitnessedSequentCalculus L (@Build_SequentCalculus L (@derivable L Gamma))) (_ : @NormalAxiomatization L minL (@Build_SequentCalculus L (@derivable L Gamma))) (_ : Typeclass_Rewrite l), G) (forall _ : Typeclass_Rewrite (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (FiniteWitnessedSequentCalculus L Gamma) fwSC) l), G) *)
  intros.
(* Goal: G *)
  apply H.
Qed.

Ltac enrich tac :=
  first
    [ tac
    | match goal with
      | |- OpaqueProp (Typeclass_Rewrite (?x :: _) -> _) =>
             apply (pop_schedule x);
             enrich tac;
             apply (push_schedule x)
      end
    ].

Ltac enrichs L tac :=
  apply (change_schedule L);
  repeat
    match goal with
    | |- OpaqueProp (Typeclass_Rewrite (?x :: _) -> _) =>
            enrich tac
    | |- OpaqueProp (Typeclass_Rewrite nil -> _) =>
            fail 1
    | |- OpaqueProp (Typeclass_Rewrite ?l -> _) =>
           fail 1000 "Cannot proceed these typeclasses: " l
    end;
  apply finish_enrich.

Ltac clear_rec L :=
  match L with
  | nil => idtac
  | exist _ _ ?H :: ?L' => clear H; clear_rec L'
  end.

Ltac AddSequentCalculus Gamma :=
  revert_dep Gamma;
  intros_dep;
  let L := schedule in
  let L' := tactic_rev L in
  enrichs L' AddSC_enrich;
  clear_rec L;
  change (@provable _ Gamma) with (@provable _ (Build_AxiomaticProofTheory provable));
  set (Gamma' := (Build_AxiomaticProofTheory provable)) in *;
  clearbody Gamma';
  clear Gamma;
  rename Gamma' into Gamma.

Ltac AddAxiomatization Gamma :=
  revert_dep Gamma;
  intros_dep;
  let L := schedule in
  let L' := tactic_rev L in
  enrichs L' AddAX_enrich;
  clear_rec L;
  change (@derivable _ Gamma) with (@derivable _ (Build_SequentCalculus derivable));
  set (Gamma' := (Build_SequentCalculus derivable)) in *;
  clearbody Gamma';
  clear Gamma;
  rename Gamma' into Gamma.

Ltac instantiate_must_succeed := instantiate (1 := _); try (instantiate (1 := _); fail 2 || fail 1).

(* Goal: DeductionWeaken L Gamma *)
(* Goal: BasicSequentCalculus L Gamma *)
Lemma MakeSequentCalculus_MinimunAxiomatization {L: Language} {minL: MinimunLanguage L} {Gamma: ProofTheory L} {minAX: MinimunAxiomatization L Gamma}:
  forall (G: Prop) (l: list (sig (fun X: Prop => X))),
  (forall
     (AX: NormalAxiomatization L (Build_AxiomaticProofTheory (@provable L Gamma)))
     (minAX: MinimunAxiomatization L (Build_AxiomaticProofTheory (@provable L Gamma)))
     (SC: NormalSequentCalculus L (Build_AxiomaticProofTheory (@provable L Gamma)))
     (bSC: BasicSequentCalculus L (Build_AxiomaticProofTheory (@provable L Gamma)))
     (fwSC: FiniteWitnessedSequentCalculus L (Build_AxiomaticProofTheory (@provable L Gamma)))
     (minSC: MinimunSequentCalculus L (Build_AxiomaticProofTheory (@provable L Gamma))),
     OpaqueProp (OpaqueProp (Typeclass_Rewrite l -> G))) <->
  OpaqueProp (Typeclass_Rewrite ((exist (fun X: Prop => X) (MinimunAxiomatization L Gamma) minAX) :: l) -> G).
Proof.
(* Goal: forall (G : Prop) (l : list (@sig Prop (fun X : Prop => X))), iff (forall (_ : FiniteWitnessedSequentCalculus L (@Build_SequentCalculus L (@derivable L Gamma))) (_ : @NormalAxiomatization L minL (@Build_SequentCalculus L (@derivable L Gamma))), OpaqueProp (OpaqueProp (forall _ : Typeclass_Rewrite l, G))) (OpaqueProp (forall _ : Typeclass_Rewrite (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (FiniteWitnessedSequentCalculus L Gamma) fwSC) l), G)) *)
  unfold OpaqueProp.
(* Goal: forall (G : Prop) (l : list (@sig Prop (fun X : Prop => X))), iff (forall (_ : FiniteWitnessedSequentCalculus L (@Build_SequentCalculus L (@derivable L Gamma))) (_ : @NormalAxiomatization L minL (@Build_SequentCalculus L (@derivable L Gamma))) (_ : Typeclass_Rewrite l), G) (forall _ : Typeclass_Rewrite (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (FiniteWitnessedSequentCalculus L Gamma) fwSC) l), G) *)
  intros.
(* Goal: forall (G : Prop) (l : list (@sig Prop (fun X : Prop => X))), iff (forall (_ : FiniteWitnessedSequentCalculus L (@Build_SequentCalculus L (@derivable L Gamma))) (_ : @NormalAxiomatization L minL (@Build_SequentCalculus L (@derivable L Gamma))) (_ : Typeclass_Rewrite l), G) (forall _ : Typeclass_Rewrite (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (FiniteWitnessedSequentCalculus L Gamma) fwSC) l), G) *)
  split; intros.
  + clear H0.
    assert (NormalAxiomatization L (Build_AxiomaticProofTheory provable))
      by (apply Build_AxiomaticProofTheory_AX).
    assert (MinimunAxiomatization L (Build_AxiomaticProofTheory provable))
      by (destruct minAX; constructor; auto).
    assert (NormalSequentCalculus L (Build_AxiomaticProofTheory provable))
      by (apply Axiomatization2SequentCalculus_SC).
    assert (BasicSequentCalculus L (Build_AxiomaticProofTheory provable))
      by (apply Axiomatization2SequentCalculus_bSC).
    assert (MinimunSequentCalculus L (Build_AxiomaticProofTheory provable))
      by (apply Axiomatization2SequentCalculus_minSC).
    assert (FiniteWitnessedSequentCalculus L (Build_AxiomaticProofTheory provable))
      by (apply Axiomatization2SequentCalculus_fwSC).
(* Goal: forall (a : @expr L) (_ : Phi a), Psi a *)
    apply H; auto.
(* Goal: Typeclass_Rewrite (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (FiniteWitnessedSequentCalculus L Gamma) fwSC) l) *)
    apply Typeclass_Rewrite_I.
(* Goal: forall (a : @expr L) (_ : Phi a), Psi a *)
  + apply H; auto.
(* Goal: Typeclass_Rewrite (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (FiniteWitnessedSequentCalculus L Gamma) fwSC) l) *)
    apply Typeclass_Rewrite_I.
Qed.

Hint Rewrite <- @MakeSequentCalculus_MinimunAxiomatization: AddSC.

(* Goal: DeductionWeaken L Gamma *)
(* Goal: BasicSequentCalculus L Gamma *)
Lemma MakeAxiomatization_BasicSequentCalculus {L: Language} {Gamma: ProofTheory L} {bSC: BasicSequentCalculus L Gamma}:
  forall (G: Prop) (l: list (sig (fun X: Prop => X))),
  (forall
     (SC: NormalSequentCalculus L (Build_SequentCalculus (@derivable L Gamma)))
     (bSC: BasicSequentCalculus L (Build_SequentCalculus (@derivable L Gamma))),
     OpaqueProp (OpaqueProp (Typeclass_Rewrite l -> G))) <->
  OpaqueProp (Typeclass_Rewrite ((exist (fun X: Prop => X) (BasicSequentCalculus L Gamma) bSC) :: l) -> G).
Proof.
(* Goal: forall (G : Prop) (l : list (@sig Prop (fun X : Prop => X))), iff (forall (_ : FiniteWitnessedSequentCalculus L (@Build_SequentCalculus L (@derivable L Gamma))) (_ : @NormalAxiomatization L minL (@Build_SequentCalculus L (@derivable L Gamma))), OpaqueProp (OpaqueProp (forall _ : Typeclass_Rewrite l, G))) (OpaqueProp (forall _ : Typeclass_Rewrite (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (FiniteWitnessedSequentCalculus L Gamma) fwSC) l), G)) *)
  unfold OpaqueProp.
(* Goal: forall (G : Prop) (l : list (@sig Prop (fun X : Prop => X))), iff (forall (_ : FiniteWitnessedSequentCalculus L (@Build_SequentCalculus L (@derivable L Gamma))) (_ : @NormalAxiomatization L minL (@Build_SequentCalculus L (@derivable L Gamma))) (_ : Typeclass_Rewrite l), G) (forall _ : Typeclass_Rewrite (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (FiniteWitnessedSequentCalculus L Gamma) fwSC) l), G) *)
  intros.
(* Goal: forall (G : Prop) (l : list (@sig Prop (fun X : Prop => X))), iff (forall (_ : FiniteWitnessedSequentCalculus L (@Build_SequentCalculus L (@derivable L Gamma))) (_ : @NormalAxiomatization L minL (@Build_SequentCalculus L (@derivable L Gamma))) (_ : Typeclass_Rewrite l), G) (forall _ : Typeclass_Rewrite (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (FiniteWitnessedSequentCalculus L Gamma) fwSC) l), G) *)
  split; intros.
  + clear H0.
    assert (NormalSequentCalculus L (Build_SequentCalculus (@derivable L Gamma)))
      by (apply Build_SequentCalculus_SC).
    assert (BasicSequentCalculus L (Build_SequentCalculus (@derivable L Gamma)))
      by (destruct bSC; constructor; auto).
(* Goal: forall (a : @expr L) (_ : Phi a), Psi a *)
    apply H; auto.
(* Goal: Typeclass_Rewrite (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (FiniteWitnessedSequentCalculus L Gamma) fwSC) l) *)
    apply Typeclass_Rewrite_I.
(* Goal: forall (a : @expr L) (_ : Phi a), Psi a *)
  + apply H; auto.
(* Goal: Typeclass_Rewrite (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (FiniteWitnessedSequentCalculus L Gamma) fwSC) l) *)
    apply Typeclass_Rewrite_I.
Qed.

Hint Rewrite <- @MakeAxiomatization_BasicSequentCalculus: AddAX.

(* Goal: DeductionWeaken L Gamma *)
(* Goal: BasicSequentCalculus L Gamma *)
Lemma MakeAxiomatization_MinimunSequentCalculus {L: Language} {minL: MinimunLanguage L} {Gamma: ProofTheory L} {minSC: MinimunSequentCalculus L Gamma} {bSC': BasicSequentCalculus L (Build_SequentCalculus (@derivable L Gamma))}:
  forall (G: Prop) (l: list (sig (fun X: Prop => X))),
  (forall
     (minSC: MinimunSequentCalculus L (Build_SequentCalculus (@derivable L Gamma)))
     (minAX: MinimunAxiomatization L (Build_SequentCalculus (@derivable L Gamma))),
     OpaqueProp (OpaqueProp (Typeclass_Rewrite l -> G))) <->
  OpaqueProp (Typeclass_Rewrite ((exist (fun X: Prop => X) (MinimunSequentCalculus L Gamma) minSC) :: l) -> G).
Proof.
(* Goal: forall (G : Prop) (l : list (@sig Prop (fun X : Prop => X))), iff (forall (_ : FiniteWitnessedSequentCalculus L (@Build_SequentCalculus L (@derivable L Gamma))) (_ : @NormalAxiomatization L minL (@Build_SequentCalculus L (@derivable L Gamma))), OpaqueProp (OpaqueProp (forall _ : Typeclass_Rewrite l, G))) (OpaqueProp (forall _ : Typeclass_Rewrite (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (FiniteWitnessedSequentCalculus L Gamma) fwSC) l), G)) *)
  unfold OpaqueProp.
(* Goal: forall (G : Prop) (l : list (@sig Prop (fun X : Prop => X))), iff (forall (_ : FiniteWitnessedSequentCalculus L (@Build_SequentCalculus L (@derivable L Gamma))) (_ : @NormalAxiomatization L minL (@Build_SequentCalculus L (@derivable L Gamma))) (_ : Typeclass_Rewrite l), G) (forall _ : Typeclass_Rewrite (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (FiniteWitnessedSequentCalculus L Gamma) fwSC) l), G) *)
  intros.
(* Goal: forall (G : Prop) (l : list (@sig Prop (fun X : Prop => X))), iff (forall (_ : FiniteWitnessedSequentCalculus L (@Build_SequentCalculus L (@derivable L Gamma))) (_ : @NormalAxiomatization L minL (@Build_SequentCalculus L (@derivable L Gamma))) (_ : Typeclass_Rewrite l), G) (forall _ : Typeclass_Rewrite (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (FiniteWitnessedSequentCalculus L Gamma) fwSC) l), G) *)
  split; intros.
  + clear H0.
    assert (NormalSequentCalculus L (Build_SequentCalculus (@derivable L Gamma)))
      by (apply Build_SequentCalculus_SC).
    assert (MinimunSequentCalculus L (Build_SequentCalculus (@derivable L Gamma)))
      by (destruct minSC; constructor; auto).
    assert (MinimunAxiomatization L (Build_SequentCalculus (@derivable L Gamma)))
      by (apply SequentCalculus2Axiomatization_minAX).
(* Goal: forall (a : @expr L) (_ : Phi a), Psi a *)
    apply H; auto.
(* Goal: Typeclass_Rewrite (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (FiniteWitnessedSequentCalculus L Gamma) fwSC) l) *)
    apply Typeclass_Rewrite_I.
(* Goal: forall (a : @expr L) (_ : Phi a), Psi a *)
  + apply H; auto.
(* Goal: Typeclass_Rewrite (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (FiniteWitnessedSequentCalculus L Gamma) fwSC) l) *)
    apply Typeclass_Rewrite_I.
Qed.

Hint Rewrite <- @MakeAxiomatization_MinimunSequentCalculus using (typeclasses eauto): AddAX.

(* Goal: DeductionWeaken L Gamma *)
(* Goal: BasicSequentCalculus L Gamma *)
Lemma MakeAxiomatization_FiniteWitnessedSequentCalculus {L: Language} {minL: MinimunLanguage L} {Gamma: ProofTheory L} {fwSC: FiniteWitnessedSequentCalculus L Gamma} {bSC': BasicSequentCalculus L (Build_SequentCalculus (@derivable L Gamma))} {minSC': MinimunSequentCalculus L (Build_SequentCalculus (@derivable L Gamma))}:
  forall (G: Prop) (l: list (sig (fun X: Prop => X))),
  (forall
     (fwSC: FiniteWitnessedSequentCalculus L (Build_SequentCalculus (@derivable L Gamma)))
     (AX: NormalAxiomatization L (Build_SequentCalculus (@derivable L Gamma))),
     OpaqueProp (OpaqueProp (Typeclass_Rewrite l -> G))) <->
  OpaqueProp (Typeclass_Rewrite ((exist (fun X: Prop => X) (FiniteWitnessedSequentCalculus L Gamma) fwSC) :: l) -> G).
Proof.
(* Goal: forall (G : Prop) (l : list (@sig Prop (fun X : Prop => X))), iff (forall (_ : FiniteWitnessedSequentCalculus L (@Build_SequentCalculus L (@derivable L Gamma))) (_ : @NormalAxiomatization L minL (@Build_SequentCalculus L (@derivable L Gamma))), OpaqueProp (OpaqueProp (forall _ : Typeclass_Rewrite l, G))) (OpaqueProp (forall _ : Typeclass_Rewrite (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (FiniteWitnessedSequentCalculus L Gamma) fwSC) l), G)) *)
  unfold OpaqueProp.
(* Goal: forall (G : Prop) (l : list (@sig Prop (fun X : Prop => X))), iff (forall (_ : FiniteWitnessedSequentCalculus L (@Build_SequentCalculus L (@derivable L Gamma))) (_ : @NormalAxiomatization L minL (@Build_SequentCalculus L (@derivable L Gamma))) (_ : Typeclass_Rewrite l), G) (forall _ : Typeclass_Rewrite (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (FiniteWitnessedSequentCalculus L Gamma) fwSC) l), G) *)
  intros.
(* Goal: forall (G : Prop) (l : list (@sig Prop (fun X : Prop => X))), iff (forall (_ : FiniteWitnessedSequentCalculus L (@Build_SequentCalculus L (@derivable L Gamma))) (_ : @NormalAxiomatization L minL (@Build_SequentCalculus L (@derivable L Gamma))) (_ : Typeclass_Rewrite l), G) (forall _ : Typeclass_Rewrite (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (FiniteWitnessedSequentCalculus L Gamma) fwSC) l), G) *)
  split; intros.
  + clear H0.
    assert (NormalSequentCalculus L (Build_SequentCalculus (@derivable L Gamma)))
      by (apply Build_SequentCalculus_SC).
    assert (FiniteWitnessedSequentCalculus L (Build_SequentCalculus (@derivable L Gamma)))
      by (destruct fwSC; constructor; auto).
    assert (NormalAxiomatization L (Build_SequentCalculus (@derivable L Gamma)))
      by (apply SequentCalculus2Axiomatization_AX).
(* Goal: forall (a : @expr L) (_ : Phi a), Psi a *)
    apply H; auto.
(* Goal: Typeclass_Rewrite (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (FiniteWitnessedSequentCalculus L Gamma) fwSC) l) *)
    apply Typeclass_Rewrite_I.
(* Goal: forall (a : @expr L) (_ : Phi a), Psi a *)
  + apply H; auto.
(* Goal: Typeclass_Rewrite (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (FiniteWitnessedSequentCalculus L Gamma) fwSC) l) *)
    apply Typeclass_Rewrite_I.
Qed.

Hint Rewrite <- @MakeAxiomatization_FiniteWitnessedSequentCalculus using (typeclasses eauto): AddAX.

Section Test_AddSC.

(* Goal: DeductionWeaken L Gamma *)
(* Goal: BasicSequentCalculus L Gamma *)
Context {L: Language}
(* Goal: DeductionWeaken L Gamma *)
(* Goal: BasicSequentCalculus L Gamma *)
        {minL: MinimunLanguage L}
(* Goal: DeductionWeaken L Gamma *)
(* Goal: BasicSequentCalculus L Gamma *)
        {Gamma: ProofTheory L}
(* Goal: DeductionWeaken L Gamma *)
(* Goal: BasicSequentCalculus L Gamma *)
        {minAX: MinimunAxiomatization L Gamma}.

Lemma provable_impp_refl': forall (x: expr), |-- x --> x.
Proof.
  AddSequentCalculus Gamma.
Abort.

End Test_AddSC.

Section Test_AddAX.

(* Goal: DeductionWeaken L Gamma *)
(* Goal: BasicSequentCalculus L Gamma *)
Context {L: Language}
(* Goal: DeductionWeaken L Gamma *)
(* Goal: BasicSequentCalculus L Gamma *)
        {minL: MinimunLanguage L}
(* Goal: DeductionWeaken L Gamma *)
(* Goal: BasicSequentCalculus L Gamma *)
        {Gamma: ProofTheory L}
(* Goal: DeductionWeaken L Gamma *)
(* Goal: BasicSequentCalculus L Gamma *)
        {bSC: BasicSequentCalculus L Gamma}
(* Goal: DeductionWeaken L Gamma *)
(* Goal: BasicSequentCalculus L Gamma *)
        {minSC: MinimunSequentCalculus L Gamma}
(* Goal: DeductionWeaken L Gamma *)
(* Goal: BasicSequentCalculus L Gamma *)
        {fwSC: FiniteWitnessedSequentCalculus L Gamma}.

Lemma derivable_axiom2': forall Phi (x y z: expr), Phi |-- (x --> y --> z) --> (x --> y) --> (x --> z).
Proof.
  AddAxiomatization Gamma.
Abort.

End Test_AddAX.
