Require Import Coq.Classes.Morphisms.
Require Import Coq.Classes.RelationClasses.
Require Import Logic.lib.Coqlib.
Require Import Logic.GeneralLogic.Base.
Require Import Logic.GeneralLogic.ProofTheory.BasicSequentCalculus.
Require Import Logic.MinimunLogic.Syntax.
Require Import Logic.MinimunLogic.ProofTheory.Minimun.
Require Import Logic.MinimunLogic.ProofTheory.RewriteClass.
Require Import Logic.PropositionalLogic.Syntax.
Require Import Logic.PropositionalLogic.ProofTheory.Intuitionistic.

Local Open Scope logic_base.
Local Open Scope syntax.
Import PropositionalLanguageNotation.

Section RewriteClass1.

Context {L: Language}
        {minL: MinimunLanguage L}
        {pL: PropositionalLanguage L}
        {Gamma: ProofTheory L}
        {minAX: MinimunAxiomatization L Gamma}
        {ipGamma: IntuitionisticPropositionalLogic L Gamma}.

Instance andp_proper_impp: Proper ((fun x y => |-- impp x y) ==> (fun x y => |-- impp x y) ==> (fun x y => |-- impp x y)) andp.
Proof.
(* Goal: @Proper (forall _ : @expr L, @expr L) (@respectful (@expr L) (@expr L) (fun x y : @expr L => @provable L Gamma (@iffp L minL pL x y)) (fun x y : @expr L => @provable L Gamma (@iffp L minL pL x y))) (@negp L minL pL) *)
  AddSequentCalculus Gamma.
(* Goal: @respectful (@expr L) Prop (fun x y : @expr L => @provable L Gamma (@iffp L minL pL x y)) iff (@derivable L Gamma Phi) (@derivable L Gamma Phi) *)
  hnf; intros x1 x2 ?.
(* Goal: @respectful (@expr L) (@expr L) (fun x y : @expr L => @provable L Gamma (@iffp L minL pL x y)) (fun x y : @expr L => @provable L Gamma (@iffp L minL pL x y)) (@iffp L minL pL x1) (@iffp L minL pL x2) *)
  hnf; intros y1 y2 ?.
(* Goal: @provable L Gamma (@iffp L minL pL (@orp L pL x1 y1) (@orp L pL x2 y2)) *)
  rewrite provable_derivable.
(* Goal: @derivable L Gamma (@empty_context L) (@impp L minL (@andp L pL x1 y1) (@andp L pL x2 y2)) *)
  rewrite <- !deduction_theorem.
(* Goal: @derivable L Gamma (Union (@expr L) (@empty_context L) (Singleton (@expr L) (@andp L pL x1 y1))) (@andp L pL x2 y2) *)
  apply (deduction_weaken0 (Union expr empty_context (Singleton expr (x1 && y1)))) in H.
(* Goal: @derivable L Gamma (Union (@expr L) (@empty_context L) (Singleton (@expr L) (@andp L pL x1 y1))) (@andp L pL x2 y2) *)
  apply (deduction_weaken0 (Union expr empty_context (Singleton expr (x1 && y1)))) in H0.
(* Goal: @derivable L Gamma (Union (@expr L) (@empty_context L) (Singleton (@expr L) (@andp L pL x1 y1))) (@andp L pL x2 y2) *)
  pose proof derivable_assum1 empty_context (x1 && y1).
(* Goal: @derivable L Gamma (Union (@expr L) (@empty_context L) (Singleton (@expr L) (@andp L pL x1 y1))) (@andp L pL x2 y2) *)
  pose proof deduction_andp_elim1 _ _ _ H1.
(* Goal: @derivable L Gamma (Union (@expr L) (@empty_context L) (Singleton (@expr L) (@andp L pL x1 y1))) (@andp L pL x2 y2) *)
  pose proof deduction_andp_elim2 _ _ _ H1.
(* Goal: @derivable L Gamma (Union (@expr L) (@empty_context L) (Singleton (@expr L) (@andp L pL x1 y1))) (@andp L pL x2 y2) *)
  pose proof deduction_modus_ponens _ _ _ H2 H.
(* Goal: @derivable L Gamma (Union (@expr L) (@empty_context L) (Singleton (@expr L) (@andp L pL x1 y1))) (@andp L pL x2 y2) *)
  pose proof deduction_modus_ponens _ _ _ H3 H0.
(* Goal: @derivable L Gamma (@empty_context L) (@iffp L minL pL y x) *)
  apply deduction_andp_intros; auto.
Qed.

Instance orp_proper_impp: Proper ((fun x y => |-- impp x y) ==> (fun x y => |-- impp x y) ==> (fun x y => |-- impp x y)) orp.
Proof.
(* Goal: @Proper (forall _ : @expr L, @expr L) (@respectful (@expr L) (@expr L) (fun x y : @expr L => @provable L Gamma (@iffp L minL pL x y)) (fun x y : @expr L => @provable L Gamma (@iffp L minL pL x y))) (@negp L minL pL) *)
  AddSequentCalculus Gamma.
(* Goal: @respectful (@expr L) Prop (fun x y : @expr L => @provable L Gamma (@iffp L minL pL x y)) iff (@derivable L Gamma Phi) (@derivable L Gamma Phi) *)
  hnf; intros x1 x2 ?.
(* Goal: @respectful (@expr L) (@expr L) (fun x y : @expr L => @provable L Gamma (@iffp L minL pL x y)) (fun x y : @expr L => @provable L Gamma (@iffp L minL pL x y)) (@iffp L minL pL x1) (@iffp L minL pL x2) *)
  hnf; intros y1 y2 ?.
(* Goal: @provable L Gamma (@iffp L minL pL x z) *)
  rewrite provable_derivable in H, H0 |- *.
(* Goal: @derivable L Gamma (@empty_context L) (@impp L minL (@orp L pL x1 y1) (@orp L pL x2 y2)) *)
  apply deduction_orp_elim'.
  + eapply deduction_impp_trans; [exact H |].
(* Goal: @derivable L Gamma (@empty_context L) (@impp L minL x2 (@orp L pL x2 y2)) *)
    apply derivable_orp_intros1.
  + eapply deduction_impp_trans; [exact H0 |].
(* Goal: @derivable L Gamma (@empty_context L) (@impp L minL y2 (@orp L pL x2 y2)) *)
    apply derivable_orp_intros2.
Qed.

Instance negp_proper_impp: Proper ((fun x y => |-- impp x y) --> (fun x y => |-- impp x y)) negp.
Proof.
(* Goal: @Proper (forall _ : @expr L, @expr L) (@respectful (@expr L) (@expr L) (fun x y : @expr L => @provable L Gamma (@iffp L minL pL x y)) (fun x y : @expr L => @provable L Gamma (@iffp L minL pL x y))) (@negp L minL pL) *)
  AddSequentCalculus Gamma.
(* Goal: @respectful (@expr L) Prop (fun x y : @expr L => @provable L Gamma (@iffp L minL pL x y)) iff (@derivable L Gamma Phi) (@derivable L Gamma Phi) *)
  hnf; intros x1 x2 ?.
(* Goal: @provable L Gamma (@iffp L minL pL (@negp L minL pL x1) (@negp L minL pL x2)) *)
  unfold negp.
(* Goal: @provable L Gamma (@impp L minL (@impp L minL x2 y2) (@impp L minL x1 y1)) *)
  apply impp_proper_impp; auto.
(* Goal: @provable L Gamma (@impp L minL (@falsep L pL) (@falsep L pL)) *)
  apply provable_impp_refl.
Qed.

Instance provable_iffp_rewrite: RewriteRelation (fun x y => |-- x <--> y).

Instance provable_iffp_equiv: Equivalence (fun x y => |-- x <--> y).
Proof.
(* Goal: @Proper (forall _ : @expr L, @expr L) (@respectful (@expr L) (@expr L) (fun x y : @expr L => @provable L Gamma (@iffp L minL pL x y)) (fun x y : @expr L => @provable L Gamma (@iffp L minL pL x y))) (@negp L minL pL) *)
  AddSequentCalculus Gamma.
(* Goal: @Equivalence (@expr L) (fun x y : @expr L => @provable L Gamma (@iffp L minL pL x y)) *)
  constructor.
  + hnf; intros.
(* Goal: @provable L Gamma (@iffp L minL pL (@orp L pL x1 y1) (@orp L pL x2 y2)) *)
    rewrite provable_derivable.
(* Goal: @derivable L Gamma (@empty_context L) (@iffp L minL pL x x) *)
    apply deduction_andp_intros; apply derivable_impp_refl.
  + hnf; intros.
(* Goal: @provable L Gamma (@iffp L minL pL y x) *)
    rewrite provable_derivable in H |- *.
(* Goal: iff (@derivable L Gamma Phi x1) (@derivable L Gamma Phi x2) *)
    pose proof deduction_andp_elim1 _ _ _ H.
(* Goal: iff (@derivable L Gamma Phi x1) (@derivable L Gamma Phi x2) *)
    pose proof deduction_andp_elim2 _ _ _ H.
(* Goal: @derivable L Gamma (@empty_context L) (@iffp L minL pL y x) *)
    apply deduction_andp_intros; auto.
  + hnf; intros.
(* Goal: @provable L Gamma (@iffp L minL pL x z) *)
    rewrite provable_derivable in H, H0 |- *.
(* Goal: iff (@derivable L Gamma Phi x1) (@derivable L Gamma Phi x2) *)
    pose proof deduction_andp_elim1 _ _ _ H.
(* Goal: iff (@derivable L Gamma Phi x1) (@derivable L Gamma Phi x2) *)
    pose proof deduction_andp_elim2 _ _ _ H.
(* Goal: @derivable L Gamma (@empty_context L) (@iffp L minL pL (@orp L pL x1 y1) (@orp L pL x2 y2)) *)
    pose proof deduction_andp_elim1 _ _ _ H0.
(* Goal: @derivable L Gamma (@empty_context L) (@iffp L minL pL (@orp L pL x1 y1) (@orp L pL x2 y2)) *)
    pose proof deduction_andp_elim2 _ _ _ H0.
(* Goal: @derivable L Gamma (@empty_context L) (@iffp L minL pL x z) *)
    apply deduction_andp_intros; eapply deduction_impp_trans; eauto.
Qed.

Instance provable_proper_iffp : Proper ((fun x y => |-- x <--> y) ==> iff) provable.
Proof.
(* Goal: @Proper (forall _ : @expr L, @expr L) (@respectful (@expr L) (@expr L) (fun x y : @expr L => @provable L Gamma (@iffp L minL pL x y)) (fun x y : @expr L => @provable L Gamma (@iffp L minL pL x y))) (@negp L minL pL) *)
  AddSequentCalculus Gamma.
(* Goal: @Proper (forall _ : @expr L, Prop) (@respectful (@expr L) Prop (fun x y : @expr L => @provable L Gamma (@iffp L minL pL x y)) iff) (@provable L Gamma) *)
  intros.
(* Goal: @Proper (forall _ : @expr L, Prop) (@respectful (@expr L) Prop (fun x y : @expr L => @provable L Gamma (@iffp L minL pL x y)) iff) (@provable L Gamma) *)
  hnf; intros.
(* Goal: @provable L Gamma (@iffp L minL pL (@orp L pL x1 y1) (@orp L pL x2 y2)) *)
  rewrite provable_derivable in H.
(* Goal: @provable L Gamma (@iffp L minL pL (@orp L pL x1 y1) (@orp L pL x2 y2)) *)
  rewrite provable_derivable.
(* Goal: @provable L Gamma (@iffp L minL pL (@orp L pL x1 y1) (@orp L pL x2 y2)) *)
  rewrite provable_derivable.
(* Goal: iff (@derivable L Gamma Phi x1) (@derivable L Gamma Phi x2) *)
  pose proof deduction_andp_elim1 _ _ _ H.
(* Goal: iff (@derivable L Gamma Phi x1) (@derivable L Gamma Phi x2) *)
  pose proof deduction_andp_elim2 _ _ _ H.
  split; intro;
  eapply deduction_modus_ponens; eauto.
Qed.

Instance impp_proper_iffp : Proper ((fun x y => |-- x <--> y) ==> (fun x y => |-- x <--> y) ==> (fun x y => |-- x <--> y)) impp.
Proof.
(* Goal: @Proper (forall _ : @expr L, @expr L) (@respectful (@expr L) (@expr L) (fun x y : @expr L => @provable L Gamma (@iffp L minL pL x y)) (fun x y : @expr L => @provable L Gamma (@iffp L minL pL x y))) (@negp L minL pL) *)
  AddSequentCalculus Gamma.
(* Goal: @respectful (@expr L) Prop (fun x y : @expr L => @provable L Gamma (@iffp L minL pL x y)) iff (@derivable L Gamma Phi) (@derivable L Gamma Phi) *)
  hnf; intros x1 x2 ?.
(* Goal: @respectful (@expr L) (@expr L) (fun x y : @expr L => @provable L Gamma (@iffp L minL pL x y)) (fun x y : @expr L => @provable L Gamma (@iffp L minL pL x y)) (@iffp L minL pL x1) (@iffp L minL pL x2) *)
  hnf; intros y1 y2 ?.
(* Goal: @provable L Gamma (@iffp L minL pL (@orp L pL x1 y1) (@orp L pL x2 y2)) *)
  rewrite provable_derivable in H.
(* Goal: @provable L Gamma (@iffp L minL pL (@orp L pL x1 y1) (@orp L pL x2 y2)) *)
  rewrite provable_derivable in H0.
(* Goal: @provable L Gamma (@iffp L minL pL (@orp L pL x1 y1) (@orp L pL x2 y2)) *)
  rewrite provable_derivable.
(* Goal: iff (@derivable L Gamma Phi x1) (@derivable L Gamma Phi x2) *)
  pose proof deduction_andp_elim1 _ _ _ H.
(* Goal: iff (@derivable L Gamma Phi x1) (@derivable L Gamma Phi x2) *)
  pose proof deduction_andp_elim2 _ _ _ H.
(* Goal: @derivable L Gamma (@empty_context L) (@iffp L minL pL (@orp L pL x1 y1) (@orp L pL x2 y2)) *)
  pose proof deduction_andp_elim1 _ _ _ H0.
(* Goal: @derivable L Gamma (@empty_context L) (@iffp L minL pL (@orp L pL x1 y1) (@orp L pL x2 y2)) *)
  pose proof deduction_andp_elim2 _ _ _ H0.
(* Goal: @derivable L Gamma (@empty_context L) (@iffp L minL pL (@orp L pL x1 y1) (@orp L pL x2 y2)) *)
  rewrite <- provable_derivable in H1.
(* Goal: @derivable L Gamma (@empty_context L) (@iffp L minL pL (@orp L pL x1 y1) (@orp L pL x2 y2)) *)
  rewrite <- provable_derivable in H2.
(* Goal: @derivable L Gamma (@empty_context L) (@iffp L minL pL (@orp L pL x1 y1) (@orp L pL x2 y2)) *)
  rewrite <- provable_derivable in H3.
(* Goal: @derivable L Gamma (@empty_context L) (@iffp L minL pL (@orp L pL x1 y1) (@orp L pL x2 y2)) *)
  rewrite <- provable_derivable in H4.
(* Goal: @derivable L Gamma (@empty_context L) (@iffp L minL pL (@orp L pL x1 y1) (@orp L pL x2 y2)) *)
  apply deduction_andp_intros; rewrite <- provable_derivable.
  + apply impp_proper_impp; auto.
  + apply impp_proper_impp; auto.
Qed.

Instance andp_proper_iffp: Proper ((fun x y => |-- x <--> y) ==> (fun x y => |-- x <--> y) ==> (fun x y => |-- x <--> y)) andp.
Proof.
(* Goal: @Proper (forall _ : @expr L, @expr L) (@respectful (@expr L) (@expr L) (fun x y : @expr L => @provable L Gamma (@iffp L minL pL x y)) (fun x y : @expr L => @provable L Gamma (@iffp L minL pL x y))) (@negp L minL pL) *)
  AddSequentCalculus Gamma.
(* Goal: @respectful (@expr L) Prop (fun x y : @expr L => @provable L Gamma (@iffp L minL pL x y)) iff (@derivable L Gamma Phi) (@derivable L Gamma Phi) *)
  hnf; intros x1 x2 ?.
(* Goal: @respectful (@expr L) (@expr L) (fun x y : @expr L => @provable L Gamma (@iffp L minL pL x y)) (fun x y : @expr L => @provable L Gamma (@iffp L minL pL x y)) (@iffp L minL pL x1) (@iffp L minL pL x2) *)
  hnf; intros y1 y2 ?.
(* Goal: @provable L Gamma (@iffp L minL pL (@orp L pL x1 y1) (@orp L pL x2 y2)) *)
  rewrite provable_derivable in H.
(* Goal: @provable L Gamma (@iffp L minL pL (@orp L pL x1 y1) (@orp L pL x2 y2)) *)
  rewrite provable_derivable in H0.
(* Goal: @provable L Gamma (@iffp L minL pL (@orp L pL x1 y1) (@orp L pL x2 y2)) *)
  rewrite provable_derivable.
(* Goal: iff (@derivable L Gamma Phi x1) (@derivable L Gamma Phi x2) *)
  pose proof deduction_andp_elim1 _ _ _ H.
(* Goal: iff (@derivable L Gamma Phi x1) (@derivable L Gamma Phi x2) *)
  pose proof deduction_andp_elim2 _ _ _ H.
(* Goal: @derivable L Gamma (@empty_context L) (@iffp L minL pL (@orp L pL x1 y1) (@orp L pL x2 y2)) *)
  pose proof deduction_andp_elim1 _ _ _ H0.
(* Goal: @derivable L Gamma (@empty_context L) (@iffp L minL pL (@orp L pL x1 y1) (@orp L pL x2 y2)) *)
  pose proof deduction_andp_elim2 _ _ _ H0.
(* Goal: @derivable L Gamma (@empty_context L) (@iffp L minL pL (@orp L pL x1 y1) (@orp L pL x2 y2)) *)
  rewrite <- provable_derivable in H1.
(* Goal: @derivable L Gamma (@empty_context L) (@iffp L minL pL (@orp L pL x1 y1) (@orp L pL x2 y2)) *)
  rewrite <- provable_derivable in H2.
(* Goal: @derivable L Gamma (@empty_context L) (@iffp L minL pL (@orp L pL x1 y1) (@orp L pL x2 y2)) *)
  rewrite <- provable_derivable in H3.
(* Goal: @derivable L Gamma (@empty_context L) (@iffp L minL pL (@orp L pL x1 y1) (@orp L pL x2 y2)) *)
  rewrite <- provable_derivable in H4.
(* Goal: @derivable L Gamma (@empty_context L) (@iffp L minL pL (@orp L pL x1 y1) (@orp L pL x2 y2)) *)
  apply deduction_andp_intros; rewrite <- provable_derivable.
  + apply andp_proper_impp; auto.
  + apply andp_proper_impp; auto.
Qed.

Instance orp_proper_iffp: Proper ((fun x y => |-- x <--> y) ==> (fun x y => |-- x <--> y) ==> (fun x y => |-- x <--> y)) orp.
Proof.
(* Goal: @Proper (forall _ : @expr L, @expr L) (@respectful (@expr L) (@expr L) (fun x y : @expr L => @provable L Gamma (@iffp L minL pL x y)) (fun x y : @expr L => @provable L Gamma (@iffp L minL pL x y))) (@negp L minL pL) *)
  AddSequentCalculus Gamma.
(* Goal: @respectful (@expr L) Prop (fun x y : @expr L => @provable L Gamma (@iffp L minL pL x y)) iff (@derivable L Gamma Phi) (@derivable L Gamma Phi) *)
  hnf; intros x1 x2 ?.
(* Goal: @respectful (@expr L) (@expr L) (fun x y : @expr L => @provable L Gamma (@iffp L minL pL x y)) (fun x y : @expr L => @provable L Gamma (@iffp L minL pL x y)) (@iffp L minL pL x1) (@iffp L minL pL x2) *)
  hnf; intros y1 y2 ?.
(* Goal: @provable L Gamma (@iffp L minL pL (@orp L pL x1 y1) (@orp L pL x2 y2)) *)
  rewrite provable_derivable in H.
(* Goal: @provable L Gamma (@iffp L minL pL (@orp L pL x1 y1) (@orp L pL x2 y2)) *)
  rewrite provable_derivable in H0.
(* Goal: @provable L Gamma (@iffp L minL pL (@orp L pL x1 y1) (@orp L pL x2 y2)) *)
  rewrite provable_derivable.
(* Goal: iff (@derivable L Gamma Phi x1) (@derivable L Gamma Phi x2) *)
  pose proof deduction_andp_elim1 _ _ _ H.
(* Goal: iff (@derivable L Gamma Phi x1) (@derivable L Gamma Phi x2) *)
  pose proof deduction_andp_elim2 _ _ _ H.
(* Goal: @derivable L Gamma (@empty_context L) (@iffp L minL pL (@orp L pL x1 y1) (@orp L pL x2 y2)) *)
  pose proof deduction_andp_elim1 _ _ _ H0.
(* Goal: @derivable L Gamma (@empty_context L) (@iffp L minL pL (@orp L pL x1 y1) (@orp L pL x2 y2)) *)
  pose proof deduction_andp_elim2 _ _ _ H0.
(* Goal: @derivable L Gamma (@empty_context L) (@iffp L minL pL (@orp L pL x1 y1) (@orp L pL x2 y2)) *)
  rewrite <- provable_derivable in H1.
(* Goal: @derivable L Gamma (@empty_context L) (@iffp L minL pL (@orp L pL x1 y1) (@orp L pL x2 y2)) *)
  rewrite <- provable_derivable in H2.
(* Goal: @derivable L Gamma (@empty_context L) (@iffp L minL pL (@orp L pL x1 y1) (@orp L pL x2 y2)) *)
  rewrite <- provable_derivable in H3.
(* Goal: @derivable L Gamma (@empty_context L) (@iffp L minL pL (@orp L pL x1 y1) (@orp L pL x2 y2)) *)
  rewrite <- provable_derivable in H4.
(* Goal: @derivable L Gamma (@empty_context L) (@iffp L minL pL (@orp L pL x1 y1) (@orp L pL x2 y2)) *)
  apply deduction_andp_intros; rewrite <- provable_derivable.
  + apply orp_proper_impp; auto.
  + apply orp_proper_impp; auto.
Qed.

Instance iffp_proper_iffp: Proper ((fun x y => |-- x <--> y) ==> (fun x y => |-- x <--> y) ==> (fun x y => |-- x <--> y)) iffp.
Proof.
(* Goal: @Proper (forall _ : @expr L, @expr L) (@respectful (@expr L) (@expr L) (fun x y : @expr L => @provable L Gamma (@iffp L minL pL x y)) (fun x y : @expr L => @provable L Gamma (@iffp L minL pL x y))) (@negp L minL pL) *)
  AddSequentCalculus Gamma.
(* Goal: @respectful (@expr L) Prop (fun x y : @expr L => @provable L Gamma (@iffp L minL pL x y)) iff (@derivable L Gamma Phi) (@derivable L Gamma Phi) *)
  hnf; intros x1 x2 ?.
(* Goal: @respectful (@expr L) (@expr L) (fun x y : @expr L => @provable L Gamma (@iffp L minL pL x y)) (fun x y : @expr L => @provable L Gamma (@iffp L minL pL x y)) (@iffp L minL pL x1) (@iffp L minL pL x2) *)
  hnf; intros y1 y2 ?.
(* Goal: @provable L Gamma (@iffp L minL pL (@iffp L minL pL x1 y1) (@iffp L minL pL x2 y2)) *)
  unfold iffp.
(* Goal: @provable L Gamma (@andp L pL (@impp L minL (@andp L pL (@impp L minL x1 y1) (@impp L minL y1 x1)) (@andp L pL (@impp L minL x2 y2) (@impp L minL y2 x2))) (@impp L minL (@andp L pL (@impp L minL x2 y2) (@impp L minL y2 x2)) (@andp L pL (@impp L minL x1 y1) (@impp L minL y1 x1)))) *)
  rewrite H, H0.
(* Goal: @provable L Gamma (@iffp L minL pL (@falsep L pL) (@falsep L pL)) *)
  apply provable_iffp_refl.
Qed.

Instance negp_proper_iffp: Proper ((fun x y => |-- x <--> y) ==> (fun x y => |-- x <--> y)) negp.
Proof.
(* Goal: @Proper (forall _ : @expr L, @expr L) (@respectful (@expr L) (@expr L) (fun x y : @expr L => @provable L Gamma (@iffp L minL pL x y)) (fun x y : @expr L => @provable L Gamma (@iffp L minL pL x y))) (@negp L minL pL) *)
  AddSequentCalculus Gamma.
(* Goal: @respectful (@expr L) Prop (fun x y : @expr L => @provable L Gamma (@iffp L minL pL x y)) iff (@derivable L Gamma Phi) (@derivable L Gamma Phi) *)
  hnf; intros x1 x2 ?.
(* Goal: @provable L Gamma (@iffp L minL pL (@negp L minL pL x1) (@negp L minL pL x2)) *)
  unfold negp.
(* Goal: @provable L Gamma (@iffp L minL pL (@impp L minL x1 (@falsep L pL)) (@impp L minL x2 (@falsep L pL))) *)
  apply impp_proper_iffp; auto.
(* Goal: @provable L Gamma (@iffp L minL pL (@falsep L pL) (@falsep L pL)) *)
  apply provable_iffp_refl.
Qed.

End RewriteClass1.

Section RewriteClass2.

Context {L: Language}
        {minL: MinimunLanguage L}
        {pL: PropositionalLanguage L}
        {Gamma: ProofTheory L}
        {SC: NormalSequentCalculus L Gamma}
        {bSC: BasicSequentCalculus L Gamma}
        {minSC: MinimunSequentCalculus L Gamma}
        {ipSC: IntuitionisticPropositionalSequentCalculus L Gamma}.

Instance derivable_proper_iffp : Proper (eq ==> (fun x y => |-- x <--> y) ==> iff) derivable.
Proof.
(* Goal: @Proper (forall (_ : @context L) (_ : @expr L), Prop) (@respectful (@context L) (forall _ : @expr L, Prop) (@eq (@context L)) (@respectful (@expr L) Prop (fun x y : @expr L => @provable L Gamma (@iffp L minL pL x y)) iff)) (@derivable L Gamma) *)
  hnf; intros Phi Phi' ?; subst Phi'.
(* Goal: @respectful (@expr L) Prop (fun x y : @expr L => @provable L Gamma (@iffp L minL pL x y)) iff (@derivable L Gamma Phi) (@derivable L Gamma Phi) *)
  hnf; intros x1 x2 ?.
(* Goal: iff (@derivable L Gamma Phi x1) (@derivable L Gamma Phi x2) *)
  apply (deduction_weaken0 Phi) in H.
(* Goal: iff (@derivable L Gamma Phi x1) (@derivable L Gamma Phi x2) *)
  pose proof deduction_andp_elim1 _ _ _ H.
(* Goal: iff (@derivable L Gamma Phi x1) (@derivable L Gamma Phi x2) *)
  pose proof deduction_andp_elim2 _ _ _ H.
  split; intro;
  eapply deduction_modus_ponens; eauto.
Qed.

End RewriteClass2.

Existing Instances andp_proper_impp orp_proper_impp negp_proper_impp
                   provable_iffp_rewrite provable_iffp_equiv
                   provable_proper_iffp derivable_proper_iffp
                   impp_proper_iffp andp_proper_iffp orp_proper_iffp iffp_proper_iffp negp_proper_iffp.
