Require Import Undecidability.FOL.Syntax.Facts.
Require Import Undecidability.FOL.Semantics.Tarski.FullFacts.
From Undecidability.FOL.Sets Require Import minZF ZF.
Require Import Undecidability.FOL.Sets.ZF.
Require Import Undecidability.FOL.Undecidability.Reductions.PCPb_to_ZF.
From Undecidability Require Import Shared.ListAutomation.
Import ListAutomationNotations.
Local Set Implicit Arguments.
Local Unset Strict Implicit.

Set Default Proof Using "Type".

Local Notation vec := Vector.t.

Local Hint Constructors prv : core.


#[local] Notation term' := (term sig_empty).
#[local] Notation form' := (form sig_empty _ _ falsity_on).

Definition embed_t (t : term') : term :=
  match t with
  | $x $x
  | func f ts False_rect term f
  end.

Fixpoint embed {ff'} (phi : form sig_empty ZF_pred_sig _ ff') : form ff' :=
  match with
  | atom P ts atom P (Vector.map embed_t ts)
  | bin b bin b (embed ) (embed )
  | quant q quant q (embed )
  |
  end.


Definition sshift {Σ_funcs : funcs_signature} k : term :=
   n match n with 0 $0 | S n $(1 + k + n) end.

Fixpoint rm_const_tm (t : term) : form' :=
  match t with
  | var n $0 ≡' var (S n)
  | func eset _ is_eset $0
  | func pair v let v' := Vector.map rm_const_tm v in
                   (Vector.hd v')[sshift 1]
                   (Vector.hd (Vector.tl v'))[sshift 2]
                   is_pair $1 $0 $2
                    | func union v (Vector.hd (Vector.map rm_const_tm v))[sshift 1] is_union $0 $1
  | func power v (Vector.hd (Vector.map rm_const_tm v))[sshift 1] is_power $0 $1
  | func omega v is_om $0
  end.

Fixpoint rm_const_fm {ff : falsity_flag} (phi : form) : form' :=
  match with
  |
  | bin bop bin sig_empty _ bop (rm_const_fm ) (rm_const_fm )
  | quant qop quant qop (rm_const_fm )
  | atom elem v let v' := Vector.map rm_const_tm v in
                   (Vector.hd v') (Vector.hd (Vector.tl v'))[sshift 1] $1 ∈'$0
  | atom equal v let v' := Vector.map rm_const_tm v in
                   (Vector.hd v') (Vector.hd (Vector.tl v'))[sshift 1] $1 ≡' $0
  end.

Definition minsolvable S :=
  rm_const_fm (solvable S).


Lemma vec_nil_eq X (v : vec X 0) :
  v = Vector.nil.
Proof.
  revert v. now apply Vector.case0.
Qed.


Lemma map_hd X Y n (f : X Y) (v : vec X (S n)) :
  Vector.hd (Vector.map f v) = f (Vector.hd v).
Proof.
  now apply (Vector.caseS' v).
Qed.


Lemma map_tl X Y n (f : X Y) (v : vec X (S n)) :
  Vector.tl (Vector.map f v) = Vector.map f (Vector.tl v).
Proof.
  now apply (Vector.caseS' v).
Qed.


Lemma in_hd X n (v : vec X (S n)) :
  Vector.In (Vector.hd v) v.
Proof.
  apply (Vector.caseS' v).
  intros. constructor.
Qed.


Lemma in_hd_tl X n (v : vec X (S (S n))) :
  Vector.In (Vector.hd (Vector.tl v)) v.
Proof.
  apply (Vector.caseS' v). intros ? w.
  apply (Vector.caseS' w).
  constructor. constructor.
Qed.


Lemma vec_inv1 X (v : vec X 1) :
  v = Vector.cons (Vector.hd v) Vector.nil.
Proof.
  apply (Vector.caseS' v). intros ?.
  now apply Vector.case0.
Qed.


Lemma vec_inv2 X (v : vec X 2) :
  v = Vector.cons (Vector.hd v) (Vector.cons (Vector.hd (Vector.tl v)) Vector.nil).
Proof.
  apply (Vector.caseS' v). intros x w.
  apply (Vector.caseS' w). intros ?.
  now apply Vector.case0.
Qed.



Section Model.

  Open Scope sem.

  Context {V : Type} {I : interp V}.

  Hypothesis M_ZF : rho, ZF'.
  Hypothesis VIEQ : extensional I.

  Instance min_model : interp sig_empty _ V.
  Proof using I.
    split.
    - intros [].
    - now apply i_atom.
  Defined.


  Lemma min_embed_eval (rho : V) (t : term') :
    eval (embed_t t) = eval t.
  Proof.
    destruct t as [|[]]. reflexivity.
  Qed.


  Lemma min_embed (rho : V) (phi : form') :
    sat I (embed ) sat min_model .
  Proof.
    induction in |- *; try destruct ; try destruct q; cbn.
    1,3-7: firstorder. erewrite Vector.map_map, Vector.map_ext.
    reflexivity. apply min_embed_eval.
  Qed.


  Lemma embed_subst_t (sigma : term') (t : term') :
    embed_t t`[] = (embed_t t)`[ >> embed_t].
  Proof.
    induction t; cbn; trivial. destruct F.
  Qed.


  Lemma embed_subst (sigma : term') (phi : form') :
    embed [] = (embed )[ >> embed_t].
  Proof.
    induction in |- *; cbn; trivial.
    - f_equal. erewrite !Vector.map_map, Vector.map_ext. reflexivity. apply embed_subst_t.
    - firstorder congruence.
    - rewrite IHphi. f_equal. apply subst_ext. intros []; cbn; trivial.
      unfold funcomp. cbn. unfold funcomp. now destruct ( n) as [x|[]].
  Qed.


  Lemma embed_sshift n (phi : form') :
    embed [sshift n] = (embed )[sshift n].
  Proof.
    rewrite embed_subst. apply subst_ext. now intros [].
  Qed.


  Lemma sat_sshift1 (rho : V) x y (phi : form') :
    (y .: x .: ) [sshift 1] (y .: ) .
  Proof.
    erewrite sat_comp, sat_ext. reflexivity. now intros [].
  Qed.


  Lemma sat_sshift2 (rho : V) x y z (phi : form') :
    (z .: y .: x .: ) [sshift 2] (z .: ) .
  Proof.
    erewrite sat_comp, sat_ext. reflexivity. now intros [].
  Qed.


  Lemma inductive_sat (rho : V) x :
    (x .: ) is_inductive $0 M_inductive x.
  Proof using VIEQ M_ZF.
    cbn. setoid_rewrite VIEQ. split.
    - destruct H as [[y Hy] _]. enough ( = y) as by apply Hy.
      apply M_ext; trivial; intros z Hz; exfalso.
      + now apply M_eset in Hz.
      + firstorder easy.
    - intros y [z Hz] % H. enough (σ y = z) as by apply Hz. apply M_ext; trivial.
      + intros a Ha % sigma_el; trivial. now apply Hz.
      + intros a Ha % Hz. now apply sigma_el.
  Qed.


  Lemma inductive_sat_om (rho : V) :
    (ω .: ) is_inductive $0.
  Proof using VIEQ M_ZF.
    cbn. setoid_rewrite VIEQ. split.
    - exists . split; try apply M_eset; trivial. now apply M_om1.
    - intros d Hd. exists (σ d). split; try now apply M_om1. intros d'. now apply sigma_el.
  Qed.


  Lemma rm_const_tm_sat (rho : V) (t : term) x :
    (x .: ) rm_const_tm t x = eval t.
  Proof using VIEQ M_ZF.
    induction t in x |- *; try destruct F; cbn; split; try intros ;
    try rewrite (vec_inv1 v); try rewrite (vec_inv2 v); cbn.
    - now rewrite VIEQ.
    - now rewrite VIEQ.
    - rewrite (vec_nil_eq (Vector.map (eval ) v)).
      intros H. apply M_ext; trivial; intros y Hy; exfalso.
      + firstorder easy.
      + now apply M_eset in Hy.
    - rewrite (vec_nil_eq (Vector.map (eval ) v)).
      intros d. now apply M_eset.
    - intros (y & Hy & z & Hz & H).
      rewrite sat_sshift1, IH in Hy; try apply in_hd. subst.
      rewrite sat_sshift2, IH in Hz; try apply in_hd_tl. subst.
      apply M_ext; trivial.
      + intros a Ha % H. rewrite !VIEQ in Ha. now apply M_pair.
      + intros a Ha % M_pair; trivial. apply H. now rewrite !VIEQ.
    - exists (eval (Vector.hd v)).
      rewrite sat_sshift1, IH; try apply in_hd. split; trivial.
      exists (eval (Vector.hd (Vector.tl v))).
      rewrite sat_sshift2, IH; try apply in_hd_tl. split; trivial.
      intros d. rewrite !VIEQ. now apply M_pair.
    - intros (y & Hy & H).
      rewrite sat_sshift1, IH in Hy; try apply in_hd. subst.
      apply M_ext; trivial.
      + intros y Hy % H. now apply M_union.
      + intros y Hy % M_union; trivial. now apply H.
    - exists (eval (Vector.hd v)).
      rewrite sat_sshift1, IH; try apply in_hd. split; trivial.
      intros d. now apply M_union.
    - intros (y & Hy & H).
      rewrite sat_sshift1, IH in Hy; try apply in_hd. subst.
      apply M_ext; trivial.
      + intros y Hy. now apply M_power, H.
      + intros y Hy. now apply H, M_power.
    - exists (eval (Vector.hd v)).
      rewrite sat_sshift1, IH; try apply in_hd. split; trivial.
      intros d. now apply M_power.
    - rewrite (vec_nil_eq (Vector.map (eval ) v)). intros [ ]. apply M_ext; trivial.
      + apply . apply (inductive_sat_om ).
      + apply M_om2; trivial. apply inductive_sat with . apply .
    - rewrite (vec_nil_eq (Vector.map (eval ) v)). split.
      + apply (inductive_sat_om ).
      + intros d Hd. apply M_om2; trivial. apply inductive_sat with . apply Hd.
  Qed.


  Lemma rm_const_sat (rho : V) (phi : form) :
     rm_const_fm .
  Proof using VIEQ M_ZF.
    induction in |- *; try destruct P; try destruct ; try destruct q; cbn.
    1,4-6: firstorder easy.
    - rewrite (vec_inv2 t). cbn. split.
      + intros H. exists (eval (Vector.hd t)). rewrite rm_const_tm_sat. split; trivial.
        exists (eval (Vector.hd (Vector.tl t))). now rewrite sat_sshift1, rm_const_tm_sat.
      + intros (x & Hx & y & Hy & H). apply rm_const_tm_sat in Hx as .
        rewrite sat_sshift1, rm_const_tm_sat in Hy. now subst.
    - rewrite (vec_inv2 t). cbn. split.
      + intros H. exists (eval (Vector.hd t)). rewrite rm_const_tm_sat. split; trivial.
        exists (eval (Vector.hd (Vector.tl t))). now rewrite sat_sshift1, rm_const_tm_sat.
      + intros (x & Hx & y & Hy & H). apply rm_const_tm_sat in Hx as .
        rewrite sat_sshift1, rm_const_tm_sat in Hy. now subst.
    - split; intros; firstorder easy.
    - firstorder eauto.
  Qed.


  Theorem min_correct (rho : V) (phi : form) :
    sat I sat min_model (rm_const_fm ).
  Proof using VIEQ M_ZF.
    apply rm_const_sat.
  Qed.


  Lemma min_axioms' (rho : V) :
     minZF'.
  Proof using VIEQ M_ZF.
    intros A [|[|[|[|[|[|[]]]]]]]; cbn.
    - apply (@M_ZF ax_ext). firstorder.
    - exists . apply (@M_ZF ax_eset). firstorder.
    - intros x y. exists ({x; y}). apply (@M_ZF ax_pair). firstorder.
    - intros x. exists ( x). apply (@M_ZF ax_union). firstorder.
    - intros x. exists (PP x). apply (@M_ZF ax_power). firstorder.
    - exists ω. split. split.
      + exists . split. apply (@M_ZF ax_eset). firstorder. apply (@M_ZF ax_om1). firstorder.
      + intros x Hx. exists (σ x). split. 2: apply (@M_ZF ax_om1); firstorder.
        intros y. rewrite !VIEQ. now apply sigma_el.
      + intros x [ ]. apply (@M_ZF ax_om2); cbn. auto 8. split.
        * destruct as (e & & ). enough ( = e) as by assumption.
          apply M_ext; trivial. all: intros y Hy; exfalso; try now apply in Hy.
          apply (@M_ZF ax_eset) in Hy; trivial. unfold ZF'. auto 8.
        * intros d (s & & ) % . enough (σ d = s) as by assumption.
          apply M_ext; trivial. all: intros y; rewrite sigma_el; trivial. all: rewrite !VIEQ; apply .
  Qed.


  Arguments subst_ext {_} {_} {_} {_} _ _ _.

  Lemma min_axioms_Z :
    ( rho phi, Z ) rho phi, minZ .
  Proof using M_ZF VIEQ.
    intros H [].
    - now apply min_axioms'.
    - cbn. specialize (H (ax_sep (embed ))). cbn in H.
      setoid_rewrite (subst_ext _ _ (($0 .: ( m : S (S (S m))) >> var) >> embed_t)) in H; try now intros [].
      rewrite embed_subst in H. setoid_rewrite min_embed in H. apply H. auto using Z.
  Qed.


  Lemma min_axioms :
    ( rho phi, ZF ) rho phi, minZF .
  Proof using M_ZF VIEQ.
    intros H [].
    - now apply min_axioms'.
    - apply min_axioms_Z; eauto using minZ. intros. apply H. destruct ; eauto using ZF.
    - cbn. specialize (H (ax_rep (embed ))). cbn in H.
      setoid_rewrite (subst_ext _ _ (($2 .: $1 .: Nat.add 3 >> var) >> embed_t)) in H at 1; try now intros [|[]].
      setoid_rewrite (subst_ext _ _ (($2 .: $0 .: Nat.add 3 >> var) >> embed_t)) in H at 2; try now intros [|[]].
      setoid_rewrite (subst_ext _ _ (($0 .: $1 .: Nat.add 4 >> var) >> embed_t)) in H at 3; try now intros [|[]].
      setoid_rewrite (subst_ext _ _ (($0 .: $1 .: Nat.add 4 >> var) >> embed_t)) in H at 4; try now intros [|[]].
      rewrite !embed_subst in H. setoid_rewrite min_embed in H. apply H. auto using ZF.
  Qed.


End Model.

Lemma ZF_to_minZF phi :
  entailment_minZF' (rm_const_fm ) entailment_ZF' .
Proof.
  intros H D M . apply min_correct; trivial.
  apply H; trivial. now apply min_axioms'.
Qed.


Lemma extensional_eq_min' V (M : @interp sig_empty _ V) rho :
  extensional M minZF' minZFeq'.
Proof.
  intros [|[|[|[|H]]]]; try now apply .
  all: cbn; intros; rewrite ! in *; congruence.
Qed.


Lemma extensional_eq_min_Z V (M : @interp sig_empty _ V) rho :
  extensional M ( phi, minZ ) ( phi, minZeq ).
Proof.
  intros []; try now apply ; auto using minZ.
  apply extensional_eq_min'; auto using minZ.
Qed.


Lemma extensional_eq_min V (M : @interp sig_empty _ V) rho :
  extensional M ( phi, minZF ) ( phi, minZFeq ).
Proof.
  intros []; try now apply ; auto using minZF.
  apply extensional_eq_min'; auto using minZF.
Qed.



Lemma up_sshift1 (phi : form') sigma :
  [sshift 1][up (up )] = [up ][sshift 1].
Proof.
  rewrite !subst_comp. apply subst_ext. intros []; trivial.
  cbn. unfold funcomp. now destruct ( n) as [|[]].
Qed.


Lemma up_sshift2 (phi : form') sigma :
  [sshift 2][up (up (up ))] = [up ][sshift 2].
Proof.
  rewrite !subst_comp. apply subst_ext. intros [|[]]; trivial.
  cbn. unfold funcomp. now destruct ( 0) as [|[]].
  cbn. unfold funcomp. now destruct as [|[]].
Qed.


Lemma rm_const_tm_subst (sigma : term') (t : term) :
  (rm_const_tm t)[up ] = rm_const_tm t`[ >> embed_t].
Proof.
  induction t; cbn; try destruct F.
  - unfold funcomp. now destruct ( x) as [k|[]].
  - reflexivity.
  - cbn. rewrite (vec_inv2 v). cbn. rewrite up_sshift2, up_sshift1, !IH; trivial. apply in_hd_tl. apply in_hd.
  - cbn. rewrite (vec_inv1 v). cbn. rewrite up_sshift1, IH; trivial. apply in_hd.
  - cbn. rewrite (vec_inv1 v). cbn. rewrite up_sshift1, IH; trivial. apply in_hd.
  - reflexivity.
Qed.


Lemma rm_const_fm_subst (sigma : term') (phi : form) :
  (rm_const_fm )[] = rm_const_fm [ >> embed_t].
Proof.
  induction in |- *; cbn; trivial; try destruct P.
  - rewrite (vec_inv2 t). cbn. now rewrite up_sshift1, !rm_const_tm_subst.
  - rewrite (vec_inv2 t). cbn. now rewrite up_sshift1, !rm_const_tm_subst.
  - firstorder congruence.
  - rewrite IHphi. f_equal. erewrite subst_ext. reflexivity. intros []; trivial.
    unfold funcomp. cbn. unfold funcomp. now destruct ( n) as [x|[]].
Qed.


Lemma rm_const_fm_shift (phi : form) :
  (rm_const_fm )[] = rm_const_fm [].
Proof.
  rewrite rm_const_fm_subst. erewrite subst_ext. reflexivity. now intros [].
Qed.


Lemma eq_sshift1 (phi : form') t :
  [sshift 1][up t..] = .
Proof.
  erewrite subst_comp, subst_id; try reflexivity. now intros [].
Qed.


Lemma eq_sshift2 (phi : form') t :
  [sshift 2][up (up t..)] = [sshift 1].
Proof.
  erewrite subst_comp, subst_ext; try reflexivity. now intros [|].
Qed.



Ltac prv_all' x :=
  apply AllI; edestruct (@nameless_equiv_all sig_empty) as [x ]; cbn; subsimpl.

Ltac use_exists' H x :=
  apply (ExE H); edestruct (@nameless_equiv_ex sig_empty) as [x ]; cbn; subsimpl.

Lemma minZF_refl' { p : peirce } t :
  minZFeq' t ≡' t.
Proof.
  change (minZFeq' ($0 ≡' $0)[t..]).
  apply AllE. apply Ctx. firstorder.
Qed.


Lemma minZF_refl { p : peirce } A t :
  minZFeq' A A t ≡' t.
Proof.
  apply Weak, minZF_refl'.
Qed.


Lemma minZF_sym { p : peirce } A x y :
  minZFeq' A A x ≡' y A y ≡' x.
Proof.
  intros HA H. assert (HS : A ax_sym'). apply Ctx. firstorder.
  apply (AllE x) in HS. cbn in HS. apply (AllE y) in HS. cbn in HS.
  subsimpl_in HS. now apply (IE HS).
Qed.


Lemma minZF_trans { p : peirce } A x y z :
  minZFeq' A A x ≡' y A y ≡' z A x ≡' z.
Proof.
  intros HA . assert (HS : A ax_trans'). apply Ctx. firstorder.
  apply (AllE x) in HS. cbn in HS. apply (AllE y) in HS. cbn in HS. apply (AllE z) in HS. cbn in HS.
  subsimpl_in HS. eapply IE. now apply (IE HS). assumption.
Qed.


Lemma minZF_elem' { p : peirce } x y u v :
  minZFeq' x ≡' u y ≡' v x ∈' y u ∈' v.
Proof.
  assert (minZFeq' ax_eq_elem'). apply Ctx. firstorder.
  apply (AllE x) in H. cbn in H. apply (AllE y) in H. cbn in H.
  apply (AllE u) in H. cbn in H. apply (AllE v) in H. cbn in H.
  subsimpl_in H. apply H.
Qed.


Lemma minZF_elem { p : peirce } A x y u v :
  minZFeq' A A x ≡' u A y ≡' v A x ∈' y A u ∈' v.
Proof.
  intros HA . eapply IE. eapply IE. eapply IE.
  eapply Weak. eapply minZF_elem'. auto. all: eauto.
Qed.


Lemma minZF_ext { p : peirce } A x y :
  minZFeq' A A sub' x y A sub' y x A x ≡' y.
Proof.
  intros HA . assert (HS : A ax_ext'). apply Ctx. firstorder.
  apply (AllE x) in HS. cbn in HS. apply (AllE y) in HS. cbn in HS.
  subsimpl_in HS. eapply IE. now apply (IE HS). assumption.
Qed.


Lemma minZF_Leibniz_tm { p : peirce } A (t : term') x y :
  minZFeq' A A x ≡' y A t`[x..] ≡' t`[y..].
Proof.
  intros HA H. destruct t as [[]|[]]; cbn; trivial. now apply minZF_refl.
Qed.


Lemma and_equiv { p : peirce } (phi psi phi' psi' : form') A :
  (A A ) (A A ) (A ) (A ).
Proof.
  intros . split; intros H % CE; apply CI; intuition.
Qed.


Lemma or_equiv { p : peirce } (phi psi phi' psi' : form') A :
  ( B, A B B B ) ( B, A B B B ) (A ) (A ).
Proof.
  intros . split; intros H; apply (DE H).
  1,3: apply DI1; apply ; auto.
  1,2: apply DI2; apply ; auto.
Qed.


Lemma impl_equiv { p : peirce } (phi psi phi' psi' : form') A :
  ( B, A B B B ) ( B, A B B B ) (A ) (A ).
Proof.
  intros . split; intros H; apply II.
  - apply ; auto. eapply IE. apply (Weak H). auto. apply ; auto.
  - apply ; auto. eapply IE. apply (Weak H). auto. apply ; auto.
Qed.


Lemma all_equiv { p : peirce } (phi psi : form') A :
  ( t, A [t..] A [t..]) (A ) (A ).
Proof.
  intros . split; intros ; apply AllI.
  all: edestruct (nameless_equiv_all A) as [x ]; apply ; auto.
Qed.


Lemma ex_equiv { p : peirce } (phi psi : form') A :
  ( B t, A B B [t..] B [t..]) (A ) (A ).
Proof.
  intros . split; intros .
  - apply (ExE ). edestruct (nameless_equiv_ex A) as [x ]. apply ExI with x. apply ; auto.
  - apply (ExE ). edestruct (nameless_equiv_ex A) as [x ]. apply ExI with x. apply ; auto.
Qed.


Lemma minZF_Leibniz { p : peirce } A (phi : form') x y :
  minZFeq' A A x ≡' y A [x..] A [y..].
Proof.
  revert A. induction using form_ind_subst; cbn; intros A HA HXY; try tauto.
  - destruct ; rewrite (vec_inv2 t); cbn; split.
    + apply minZF_elem; trivial; now apply minZF_Leibniz_tm.
    + apply minZF_sym in HXY; trivial. apply minZF_elem; trivial; now apply minZF_Leibniz_tm.
    + intros H. eapply minZF_trans; trivial. apply minZF_Leibniz_tm; trivial. eapply minZF_sym; eauto.
      eapply minZF_trans; trivial. apply H. now apply minZF_Leibniz_tm.
    + intros H. eapply minZF_trans; trivial. apply minZF_Leibniz_tm; eauto.
      eapply minZF_trans; trivial. apply H. apply minZF_Leibniz_tm; trivial. now apply minZF_sym.
  - destruct .
    + apply and_equiv; firstorder easy.
    + apply or_equiv; intros B HB.
      * apply . now rewrite HA. now apply (Weak HXY).
      * apply . now rewrite HA. now apply (Weak HXY).
    + apply impl_equiv; intros B HB.
      * apply . now rewrite HA. now apply (Weak HXY).
      * apply . now rewrite HA. now apply (Weak HXY).
  - destruct x as [n|[]], y as [m|[]]. destruct q.
    + apply all_equiv. intros [k|[]]. specialize (H ($(S k)..) A HA HXY).
      erewrite !subst_comp, subst_ext, subst_comp. rewrite H.
      erewrite !subst_comp, subst_ext. reflexivity. all: now intros [|[]]; cbn.
    + apply ex_equiv. intros B [k|[]] HB. cbn. specialize (H ($(S k)..) B).
      erewrite !subst_comp, subst_ext, subst_comp. rewrite H. 2: now rewrite HA. 2: now apply (Weak HXY).
      erewrite !subst_comp, subst_ext. reflexivity. all: now intros [|[]]; cbn.
Qed.


Lemma iff_equiv { p : peirce } (phi psi phi' psi' : form') A :
  ( B, A B B B ) ( B, A B B B ) (A ) (A ).
Proof.
  intros . split; intros [ ] % CE; apply CI; eapply impl_equiv.
  3,9: apply . 5,10: apply . all: firstorder.
Qed.



Lemma prv_ex_eq { p : peirce } A x phi :
  minZFeq' A A [x..] A $0 ≡' x`[] .
Proof.
  intros HA. split; intros H.
  - apply (ExI x). cbn. subsimpl. apply CI; trivial. now apply minZF_refl.
  - use_exists' H y. eapply minZF_Leibniz; eauto 3. apply minZF_sym; eauto 3.
Qed.


Lemma use_ex_eq { p : peirce } A x phi psi :
  minZFeq' A A [x..] A ( $0 ≡' x`[] ) .
Proof.
  intros H. apply impl_equiv; try tauto. intros B HB. apply prv_ex_eq. now rewrite H.
Qed.


Local Ltac simpl_ex :=
  try apply prv_ex_eq; try apply use_ex_eq; auto; cbn; subsimpl.

Local Ltac simpl_ex_in H :=
  try apply prv_ex_eq in H; try apply use_ex_eq in H; auto; cbn in H; subsimpl_in H.

Lemma prv_to_min_refl { p : peirce } :
  minZFeq' rm_const_fm ax_refl.
Proof.
  prv_all x. repeat simpl_ex. apply minZF_refl'.
Qed.


Lemma prv_to_min_sym { p : peirce } :
  minZFeq' rm_const_fm ax_sym.
Proof.
  prv_all x. prv_all y. apply II. H. use_exists' H a. H'.
  apply CE2 in H'. use_exists' H' b. repeat simpl_ex. eapply minZF_trans; auto.
  - apply minZF_sym; auto. eapply CE1. auto.
  - eapply minZF_trans; auto. apply minZF_sym; auto. eapply CE2. auto. eapply CE1, Ctx. auto.
Qed.


Lemma prv_to_min_trans { p : peirce } :
  minZFeq' rm_const_fm ax_trans.
Proof.
  prv_all x. prv_all y. prv_all z.
  repeat simpl_ex. apply II. repeat simpl_ex. apply II.
  repeat simpl_ex. eapply minZF_trans; auto.
Qed.


Lemma prv_to_min_elem { p : peirce } :
  minZFeq' rm_const_fm ax_eq_elem.
Proof.
  prv_all x. prv_all y. prv_all u. prv_all v.
  repeat simpl_ex. apply II. repeat simpl_ex. apply II. repeat simpl_ex. apply II.
  repeat simpl_ex. eapply minZF_elem; auto.
Qed.


Lemma prv_to_min_ext { p : peirce } :
  minZFeq' rm_const_fm ax_ext.
Proof.
  prv_all x. prv_all y. apply II. apply II.
  repeat simpl_ex. apply minZF_ext; auto; prv_all z; apply II.
  - H. apply (AllE z) in H. cbn in H. subsimpl_in H.
    repeat simpl_ex_in H. rewrite imps in H.
    repeat simpl_ex_in H. apply (Weak H). auto.
  - H. apply (AllE z) in H. cbn in H. subsimpl_in H.
    repeat simpl_ex_in H. rewrite imps in H.
    repeat simpl_ex_in H. apply (Weak H). auto.
Qed.


Lemma prv_to_min_eset { p : peirce } :
  minZFeq' rm_const_fm ax_eset.
Proof.
  prv_all x. simpl_ex. apply II.
   H. use_exists' H y. clear H. eapply IE. 2: eapply CE2, Ctx; auto 1.
   H. apply CE1 in H. apply (AllE x) in H. cbn in H. now subsimpl_in H.
Qed.


Lemma prv_to_min_pair { p : peirce } :
  minZFeq' rm_const_fm ax_pair.
Proof.
  prv_all x. prv_all y. prv_all z. apply CI.
  - simpl_ex. apply II.
     H. use_exists' H u. clear H. H. apply CE in H as [ ].
    repeat simpl_ex_in . apply (AllE z) in . cbn in . subsimpl_in .
    apply CE1 in . apply (IE ) in . apply (DE ); [apply DI1 | apply DI2].
    all: repeat simpl_ex.
  - assert (HP : minZFeq' ax_pair') by (apply Ctx; firstorder).
    apply (AllE y) in HP. cbn in HP. apply (AllE x) in HP. cbn in HP. use_exists' HP u. clear HP. apply II.
    simpl_ex. apply (ExI u). cbn. subsimpl. apply CI.
    + repeat simpl_ex.
    + H. apply (AllE z) in H. cbn in H. subsimpl_in H. apply CE2 in H. apply (IE H). clear H. eapply DE.
      * apply Ctx. auto.
      * apply DI1. H. repeat simpl_ex_in H.
      * apply DI2. H. repeat simpl_ex_in H.
Qed.


Lemma prv_to_min_union { p : peirce } :
  minZFeq' rm_const_fm ax_union.
Proof.
  prv_all x. prv_all y. apply CI.
  - simpl_ex. apply II.
     H. use_exists' H u. clear H. H. apply CE in H as [ ].
    simpl_ex_in . apply (AllE y) in . cbn in . subsimpl_in .
    apply CE1 in . apply (IE ) in . use_exists' z.
    apply (ExI z). cbn. subsimpl. apply CI; repeat simpl_ex.
    + eapply CE1. auto.
    + eapply CE2. auto.
  - assert (HU : minZFeq' ax_union') by (apply Ctx; firstorder).
    apply (AllE x) in HU. cbn in HU. use_exists' HU u.
    apply II. H. use_exists' H z. clear H. H. apply CE in H as [ ].
    repeat simpl_ex_in . repeat simpl_ex_in . simpl_ex.
    apply (ExI u). cbn. subsimpl. apply CI.
    + simpl_ex. apply Ctx. auto.
    + Hu. apply (AllE y) in Hu. cbn in Hu. subsimpl_in Hu. apply CE2 in Hu.
      apply (IE Hu). apply (ExI z). cbn. subsimpl. now apply CI.
Qed.


Lemma prv_to_min_power { p : peirce } :
  minZFeq' rm_const_fm ax_power.
Proof.
  prv_all x. prv_all y. apply CI.
  - simpl_ex. apply II.
     H. use_exists' H u. clear H. H. apply CE in H as [ ].
    simpl_ex_in . apply (AllE y) in . cbn in . subsimpl_in .
    apply CE1 in . apply (IE ) in . prv_all z.
    repeat simpl_ex. apply II. repeat simpl_ex. apply imps.
    apply (AllE z) in . cbn in . now subsimpl_in .
  - assert (HP : minZFeq' ax_power') by (apply Ctx; firstorder).
    apply (AllE x) in HP. cbn in HP. use_exists' HP u. clear HP. apply II.
    simpl_ex. apply (ExI u). cbn. subsimpl. apply CI.
    + simpl_ex. apply Ctx. auto.
    + H. apply (AllE y) in H. cbn in H. subsimpl_in H. apply CE2 in H. apply (IE H). clear H.
      prv_all z. apply II. H. apply (AllE z) in H. cbn in H. subsimpl_in H.
      repeat simpl_ex_in H. rewrite imps in H. repeat simpl_ex_in H. apply (Weak H). auto 8.
Qed.


Lemma prv_to_min_inductive { p : peirce } A n :
  minZFeq' A A rm_const_fm (inductive $n) A is_inductive $n.
Proof.
  cbn. intros HA HI. apply CI.
  - apply CE1 in HI. use_exists' HI x. clear HI.
    apply (ExI x). cbn. H. apply CE in H as [ ]. apply CI; trivial.
    change ( $0 ≡' n x`[] ∈' $0) with ( $0 ≡' $n`[] x`[] ∈' $0) in .
    now simpl_ex_in .
  - apply CE2 in HI. prv_all x. apply (AllE x) in HI. cbn in HI. simpl_ex_in HI.
    change ( $0 ≡' n x`[] ∈' $0) with ( $0 ≡' $n`[] x`[] ∈' $0) in HI.
    simpl_ex_in HI. rewrite imps in *. use_exists' HI y. clear HI.
     H. apply (ExI y). cbn. subsimpl. apply CI.
    + apply CE1 in H. use_exists' H a. clear H. H. apply CE in H as [ ].
      simpl_ex_in . prv_all b. apply (AllE b) in . cbn in . subsimpl_in .
      eapply iff_equiv; try apply ; try tauto.
      intros B HB. clear . eapply Weak in ; try apply HB. split; intros .
      * use_exists' z. clear . H. apply CE in H as [H H'].
        apply prv_ex_eq in H; try rewrite HB; auto. cbn in H. subsimpl_in H.
        apply prv_ex_eq in H; try rewrite HB; auto. cbn in H. subsimpl_in H.
        eapply Weak in . apply (DE ). 3: auto.
        -- apply (ExI x). cbn. subsimpl. apply CI; auto. apply (AllE x) in H'. cbn in H'. subsimpl_in H'.
           apply CE2 in H'. eapply IE. apply (Weak H'); auto. apply DI1. apply minZF_refl. rewrite HB. auto 6.
        -- apply (ExI z). cbn. subsimpl. apply CI.
           ++ apply (AllE z) in H'. cbn in H'. subsimpl_in H'. apply CE2 in H'. eapply IE.
              apply (Weak H'); auto. apply DI2. apply minZF_refl. rewrite HB. auto 6.
           ++ apply (AllE b) in H. cbn in H. subsimpl_in H. apply CE2 in H. eapply IE.
              apply (Weak H); auto. apply DI2. auto.
      * use_exists' z. clear . H. apply CE in H as [H H'].
        apply prv_ex_eq in H; try rewrite HB; auto. cbn in H. subsimpl_in H.
        apply prv_ex_eq in H; try rewrite HB; auto. cbn in H. subsimpl_in H.
        eapply Weak in . use_exists' c. 2: auto. clear . . apply CE in as [ ].
        apply (AllE c) in H'. cbn in H'. subsimpl_in H'. apply CE1 in H'. eapply Weak in H'.
        apply (IE H') in . 2: auto. clear H'. apply (DE ).
        -- apply DI1. eapply minZF_elem. rewrite HB, HA. auto 8. 3: apply (Weak ); auto.
           2: auto. apply minZF_refl. rewrite HB, HA. auto 8.
        -- apply DI2. apply (AllE b) in H. cbn in H. subsimpl_in H. apply CE1 in H. eapply DE'.
           eapply IE. apply (Weak H). auto. eapply minZF_elem. rewrite HB, HA. auto 8.
           3: apply (Weak ); auto. 2: auto. apply minZF_refl. rewrite HB, HA. auto 8.
    + apply CE2 in H. change ( $0 ≡' n y`[] ∈' $0) with ( $0 ≡' $n`[] y`[] ∈' $0) in H.
      now simpl_ex_in H.
Qed.


Lemma inductive_subst t sigma :
  (inductive t)[] = inductive t`[].
Proof.
  cbn. subsimpl. reflexivity.
Qed.


Lemma is_inductive_subst t sigma :
  (is_inductive t)[] = is_inductive t`[].
Proof.
  cbn. subsimpl. reflexivity.
Qed.


Lemma is_om_subst t sigma :
  (is_om t)[] = is_om t`[].
Proof.
  cbn. subsimpl. reflexivity.
Qed.


Local Arguments is_om : simpl never.
Local Arguments is_inductive : simpl never.

Lemma is_eset_sub { p : peirce } A x y :
  minZFeq' A A is_eset x A sub' x y.
Proof.
  intros HA HE. prv_all z. apply II, Exp, IE with (($0 ∈' x`[])[z..]).
  - change ((z ∈' x :: A) (¬ $0 ∈' x`[])[z..]). apply AllE, (Weak HE). auto.
  - cbn. subsimpl. auto.
Qed.


Lemma is_eset_unique { p : peirce } A x y :
  minZFeq' A A is_eset x A is_eset y A x ≡' y.
Proof.
  intros HA . apply minZF_ext; auto; now apply is_eset_sub.
Qed.


Lemma prv_to_min_om1 { p : peirce } :
  minZFeq' rm_const_fm ax_om1.
Proof.
  apply CI.
  - assert (HO : minZFeq' ax_om') by (apply Ctx; firstorder).
    use_exists' HO o. clear HO.
    assert (HE : minZFeq' ax_eset') by (apply Ctx; firstorder).
    eapply Weak in HE. use_exists' HE e. clear HE. 2: auto.
    apply (ExI e). cbn. apply CI; auto. apply (ExI o). cbn. subsimpl. rewrite eq_sshift1.
    apply CI; auto. H. unfold is_om in H at 2. cbn in H. apply CE1 in H.
    rewrite is_inductive_subst in H. cbn in H. apply CE1 in H. use_exists' H e'. clear H.
     H. apply CE in H as [ ]. eapply minZF_elem; auto; try eassumption.
    2: apply minZF_refl; auto. apply is_eset_unique; auto.
  - prv_all x. simpl_ex. rewrite up_sshift1, eq_sshift1, !is_om_subst. cbn.
    apply II. H. use_exists' H o. clear H. H. apply CE in H as [ ].
    unfold is_om in at 3. cbn in . apply CE1 in . unfold is_inductive in . cbn in . apply CE2 in .
    apply (AllE x) in . cbn in . subsimpl_in . apply (IE ) in . use_exists' y. clear .
    apply (ExI y). cbn. subsimpl. apply CI.
    + assert (HP : minZFeq' ax_pair') by (apply Ctx; firstorder).
      apply (AllE x) in HP. cbn in HP. subsimpl_in HP. apply (AllE x) in HP. cbn in HP. subsimpl_in HP.
      eapply Weak in HP. use_exists' HP s. 2: auto. clear HP.
      assert (HP : minZFeq' ax_pair') by (apply Ctx; firstorder).
      apply (AllE x) in HP. cbn in HP. subsimpl_in HP. apply (AllE s) in HP. cbn in HP. subsimpl_in HP.
      eapply Weak in HP. use_exists' HP t. 2: auto. clear HP.
      apply (ExI t). cbn. subsimpl. apply CI.
      * apply prv_ex_eq; auto 7. apply (ExI s). cbn. subsimpl. apply CI; auto.
        apply prv_ex_eq; auto 7. cbn. subsimpl. apply prv_ex_eq; auto 7. cbn. subsimpl. auto.
      * prv_all z. H. apply CE1, (AllE z) in H. cbn in H. subsimpl_in H.
        apply CE in H as [ ]. apply CI; rewrite imps in *.
        -- clear . apply (DE ); clear .
           ++ apply (ExI x). cbn. subsimpl. apply CI; auto. H. apply (AllE x) in H. cbn in H. subsimpl_in H.
              apply CE2 in H. apply (IE H). apply DI1. apply minZF_refl. auto 8.
           ++ apply (ExI s). cbn. subsimpl. apply CI.
              ** H. apply (AllE s) in H. cbn in H. subsimpl_in H.
                 apply CE2 in H. apply (IE H). apply DI2. apply minZF_refl. auto 8.
              ** H. apply (AllE z) in H. cbn in H. subsimpl_in H.
                 apply CE2 in H. apply (IE H). apply DI1. auto.
        -- rewrite imps in . eapply Weak in . apply (IE ). 2: auto. clear .
            H. use_exists' H a. clear H. H. apply CE in H as [ ].
            H. apply (AllE a) in H. cbn in H. subsimpl_in H.
           apply CE1 in H. apply (IE H) in . clear H. apply (DE ).
           ** apply DI1. eapply minZF_elem; auto 9. 2: apply (Weak ); auto. apply minZF_refl. auto 9.
           ** apply DI2. apply DE'. apply IE with (z ∈' s). eapply CE1 with (z ≡' x z ≡' x z ∈' s).
              replace (z ∈' s z ≡' x z ≡' x) with (($0 ∈' s`[] $0 ≡' x`[] $0 ≡' x`[])[z..]).
              2: cbn; now subsimpl. apply AllE. auto 7. eapply minZF_elem; auto 9.
              2: apply (Weak ); auto. apply minZF_refl. auto 9.
    + apply (ExI o). cbn. subsimpl. rewrite !is_om_subst. cbn. apply CI; [eapply CE1 | eapply CE2]; auto.
Qed.


Local Arguments inductive : simpl never.
Local Arguments is_om : simpl nomatch.

Lemma prv_to_min_om2 { p : peirce } :
  minZFeq' rm_const_fm ax_om2.
Proof.
  cbn. prv_all x. destruct x as [n|[]]. cbn. rewrite rm_const_fm_subst, inductive_subst, !is_inductive_subst.
  cbn. apply II. prv_all m. cbn. rewrite !is_inductive_subst. cbn. simpl_ex.
  rewrite !is_inductive_subst. cbn. apply II. simpl_ex.
  change ( $0 ≡' n m`[] ∈' $0) with ( $0 ≡' $n`[] m`[] ∈' $0).
  simpl_ex. H. use_exists' H k. clear H.
  cbn. rewrite !is_inductive_subst. cbn. subsimpl. H. apply CE in H as [ % CE2 ].
  apply (AllE $n) in . cbn in . subsimpl_in . rewrite is_inductive_subst in . cbn in .
   . apply prv_to_min_inductive in ; auto. apply (IE ) in .
  apply (AllE m) in . cbn in . subsimpl_in . now apply (IE ).
Qed.


Lemma prv_to_min { p : peirce } phi :
   ZFeq' minZFeq' rm_const_fm .
Proof.
  intros [|[|[|[|[|[|[|[|[|[|[|[]]]]]]]]]]]].
  - apply prv_to_min_refl.
  - apply prv_to_min_sym.
  - apply prv_to_min_trans.
  - apply prv_to_min_elem.
  - apply prv_to_min_ext.
  - apply prv_to_min_eset.
  - apply prv_to_min_pair.
  - apply prv_to_min_union.
  - apply prv_to_min_power.
  - apply prv_to_min_om1.
  - apply prv_to_min_om2.
Qed.



Section Deduction.

  Lemma rm_const_tm_prv { p : peirce } t :
    minZFeq' rm_const_tm t.
  Proof.
    induction t; try destruct F; cbn.
    - apply (ExI $x). cbn. apply minZF_refl'.
    - apply Ctx. firstorder.
    - rewrite (vec_inv2 v). cbn.
      assert ( : minZFeq' rm_const_tm (Vector.hd v)) by apply IH, in_hd.
      assert ( : minZFeq' rm_const_tm (Vector.hd (Vector.tl v))) by apply IH, in_hd_tl.
      use_exists' x. eapply Weak in . use_exists' y. 2: auto.
      assert (H : minZFeq' ax_pair') by (apply Ctx; firstorder).
      apply (AllE x) in H. cbn in H. apply (AllE y) in H. cbn in H.
      eapply Weak in H. use_exists' H z. 2: auto. apply (ExI z). cbn.
      apply (ExI x). cbn. subsimpl. rewrite eq_sshift1. apply CI; auto.
      apply (ExI y). cbn. subsimpl. erewrite !subst_comp, subst_ext. apply CI; auto. now intros [].
    - rewrite (vec_inv1 v). cbn. specialize (IH _ (in_hd v)). use_exists' IH x.
      assert (H : minZFeq' ax_union') by (apply Ctx; firstorder). apply (AllE x) in H. cbn in H.
      eapply Weak in H. use_exists' H y. 2: auto. apply (ExI y). cbn. apply (ExI x). cbn. subsimpl.
      rewrite eq_sshift1. apply CI; auto.
    - rewrite (vec_inv1 v). cbn. specialize (IH _ (in_hd v)). use_exists' IH x.
      assert (H : minZFeq' ax_power') by (apply Ctx; firstorder). apply (AllE x) in H. cbn in H.
      eapply Weak in H. use_exists' H y. 2: auto. apply (ExI y). cbn. apply (ExI x). cbn. subsimpl.
      rewrite eq_sshift1. apply CI; auto.
    - apply Ctx. firstorder.
  Qed.


  Lemma rm_const_tm_sub { p : peirce } A t (x y : term') :
    minZFeq' A A (rm_const_tm t)[x..] A (rm_const_tm t)[y..] A sub' x y.
  Proof.
    intros HA. induction t in A, HA, x, y |- *; try destruct F; cbn -[is_inductive sub'].
    - intros . prv_all z. apply II. eapply minZF_elem; auto; try apply minZF_refl; auto.
      eapply minZF_trans; auto. apply (Weak ); auto. apply minZF_sym; auto. apply (Weak ). auto.
    - intros H _. prv_all z. apply II. apply Exp. apply (AllE z) in H. cbn in H. subsimpl_in H.
      eapply IE; try apply (Weak H); auto.
    - rewrite (vec_inv2 v). cbn. rewrite !eq_sshift1. intros . prv_all a. apply II.
      eapply Weak in . use_exists' b. 2: auto. clear . H. apply CE in H as [ ].
      eapply Weak in . use_exists' c. 2: auto. clear . H. apply CE in H as [ ].
      eapply Weak in . use_exists' d. 2: auto. clear . H. apply CE in H as [ ].
      eapply Weak in . use_exists' e. 2: auto. clear . H. apply CE in H as [ ].

      pose (B := ((rm_const_tm (Vector.hd v))[b..]
            ( (rm_const_tm (Vector.hd (Vector.tl v)))[sshift 2][up (up x..)][up b..]
                 ( $0 ∈' x`[]`[] $0 ≡' b`[]`[] $0 ≡' 0)) :: a ∈' x :: A)).
      fold B in , , , , , . fold B. rewrite !eq_sshift2, !eq_sshift1 in *.

      assert (HB : minZFeq' B). { rewrite HA. unfold B. auto. }
      apply (AllE a) in . cbn in . subsimpl_in . eapply IE. eapply CE2. apply .
      apply (AllE a) in . cbn in . subsimpl_in . eapply DE.
      + eapply IE. eapply CE1. apply (Weak ); auto. apply Ctx. unfold B. auto.
      + apply DI1. eapply minZF_trans; auto. apply minZF_ext; auto.
        * eapply (IH _ (in_hd v)); auto; eapply Weak. apply . auto. apply . auto.
        * eapply (IH _ (in_hd v)); auto; eapply Weak. apply . auto. apply . auto.
      + apply DI2. eapply minZF_trans; auto. apply minZF_ext; auto.
        * eapply (IH _ (in_hd_tl v)); auto; eapply Weak. apply . auto. apply . auto.
        * eapply (IH _ (in_hd_tl v)); auto; eapply Weak. apply . auto. apply . auto.
    - rewrite (vec_inv1 v). cbn. rewrite !eq_sshift1 in *. intros .
      prv_all a. apply II. eapply Weak in . use_exists' b. 2: auto.
      eapply Weak in . use_exists' c. 2: auto. clear .
       H. apply CE in H as [ ]. apply (AllE a) in . cbn in . subsimpl_in .
      eapply IE. eapply CE2, . clear .
       H. apply CE in H as [ ]. apply (AllE a) in . cbn in . subsimpl_in .
      apply CE1 in . . apply (IE ) in . use_exists' d. clear .
      apply (ExI d). cbn. subsimpl. apply CI. 2: eapply CE2; auto.
      eapply (IH _ (in_hd v) _ b c) in ; auto. apply (AllE d) in . cbn in . subsimpl_in .
      eapply Weak in . apply (IE ). 2: auto. eapply CE1; auto.
    - rewrite (vec_inv1 v). cbn. rewrite !eq_sshift1. intros .
      prv_all a. apply II. eapply Weak in . use_exists' b. 2: auto.
      eapply Weak in . use_exists' c. 2: auto. clear .
       H. apply CE in H as [ ]. apply (AllE a) in . cbn in . subsimpl_in .
      eapply IE. eapply CE2, . clear .
       H. apply CE in H as [ ]. apply (AllE a) in . cbn in . subsimpl_in .
      apply CE1 in . . apply (IE ) in . clear .
      prv_all d. apply II. apply (IH _ (in_hd v) _ b c) in ; auto. apply (AllE d) in . cbn in . subsimpl_in .
      eapply Weak in . apply (IE ). 2: auto. apply (AllE d) in . cbn in . subsimpl_in .
      eapply Weak in . apply (IE ). all: auto.
    - intros [ ] % CE [ ] % CE. apply (AllE y) in .
      cbn -[is_inductive] in . subsimpl_in . apply (IE ). apply .
  Qed.


  Lemma rm_const_tm_equiv { p : peirce } A t (x y : term') :
    minZFeq' A A (rm_const_tm t)[x..] A y ≡' x A (rm_const_tm t)[y..].
  Proof.
    intros HA Hx. split; intros H.
    - eapply minZF_Leibniz; eauto.
    - apply minZF_ext; trivial; eapply rm_const_tm_sub; eauto.
  Qed.


  Lemma rm_const_tm_swap { p : peirce } A t s x a :
    minZFeq' A A (rm_const_tm t)[x..] A (rm_const_tm s)[a.:x..] A (rm_const_tm s`[t..])[a..].
  Proof.
    induction s in A, a, x |- *; cbn; try destruct F; cbn; intros HA Hx; try tauto.
    - destruct ; cbn; try tauto. now apply rm_const_tm_equiv.
    - rewrite (vec_inv2 v). cbn. apply ex_equiv. intros B y HB. cbn. apply and_equiv.
      + erewrite !subst_comp, subst_ext. setoid_rewrite subst_ext at 2.
        apply IH; try apply in_hd. now rewrite HA. now apply (Weak Hx).
        all: intros [|[]]; cbn; try reflexivity. apply subst_term_shift.
      + apply ex_equiv. intros C z HC. cbn. apply and_equiv; try tauto.
        erewrite !subst_comp, subst_ext. setoid_rewrite subst_ext at 2.
        apply IH; try apply in_hd_tl. now rewrite HA, HB. apply (Weak Hx). now rewrite HB.
        all: intros [|[]]; cbn; try reflexivity.
        rewrite !subst_term_comp. now apply subst_term_id.
    - rewrite (vec_inv1 v). cbn. apply ex_equiv. intros B y HB. cbn. apply and_equiv; try tauto.
      erewrite !subst_comp, subst_ext. setoid_rewrite subst_ext at 2.
      apply IH; try apply in_hd. now rewrite HA. now apply (Weak Hx).
      all: intros [|[]]; cbn; try reflexivity. apply subst_term_shift.
    - rewrite (vec_inv1 v). cbn. apply ex_equiv. intros B y HB. cbn. apply and_equiv; try tauto.
      erewrite !subst_comp, subst_ext. setoid_rewrite subst_ext at 2.
      apply IH; try apply in_hd. now rewrite HA. now apply (Weak Hx).
      all: intros [|[]]; cbn; try reflexivity. apply subst_term_shift.
  Qed.


  Lemma rm_const_fm_swap { p : peirce } A phi t x :
    minZFeq' A A (rm_const_tm t)[x..] A (rm_const_fm )[x..] A rm_const_fm [t..].
  Proof.
    revert A. induction using form_ind_subst; cbn; intros A HA Hx.
    all: try destruct ; try destruct ; try destruct q; try tauto.
    - rewrite (vec_inv2 ). cbn. apply ex_equiv. cbn. intros B a HB. apply and_equiv.
      + rewrite subst_comp. erewrite subst_ext.
        * eapply rm_const_tm_swap. now rewrite HA. now apply (Weak Hx).
        * intros [|[|]]; trivial. now destruct x as [|[]].
      + apply ex_equiv. cbn. intros C a' HC. apply and_equiv; try tauto.
        rewrite !subst_comp. erewrite subst_ext. setoid_rewrite subst_ext at 2.
        * eapply rm_const_tm_swap. now rewrite HA, HB. apply (Weak Hx). now rewrite HB.
        * intros [|[]]; reflexivity.
        * intros [|[]]; trivial. now destruct x as [|[]].
    - rewrite (vec_inv2 ). cbn. apply ex_equiv. cbn. intros B a HB. apply and_equiv.
      + rewrite subst_comp. erewrite subst_ext.
        * eapply rm_const_tm_swap. now rewrite HA. now apply (Weak Hx).
        * intros [|[|]]; trivial. now destruct x as [|[]].
      + apply ex_equiv. cbn. intros C a' HC. apply and_equiv; try tauto.
        rewrite !subst_comp. erewrite subst_ext. setoid_rewrite subst_ext at 2.
        * eapply rm_const_tm_swap. now rewrite HA, HB. apply (Weak Hx). now rewrite HB.
        * intros [|[]]; reflexivity.
        * intros [|[]]; trivial. now destruct x as [|[]].
    - apply and_equiv; firstorder easy.
    - apply or_equiv; intros B HB.
      + apply . now rewrite HA. now apply (Weak Hx).
      + apply . now rewrite HA. now apply (Weak Hx).
    - apply impl_equiv; intros B HB.
      + apply . now rewrite HA. now apply (Weak Hx).
      + apply . now rewrite HA. now apply (Weak Hx).
    - apply all_equiv. intros [n|[]]. destruct x as [m|[]].
      assert (A (rm_const_fm [$(S n)..])[$m..] A (rm_const_fm [$(S n)..][t..])) by now apply H, (Weak Hx).
      erewrite subst_comp, subst_ext, subst_comp, (rm_const_fm_subst ($(S n)..)). setoid_rewrite subst_ext at 2.
      rewrite . erewrite rm_const_fm_subst, !subst_comp, subst_ext. reflexivity.
      all: intros [|[]]; cbn; try reflexivity. rewrite subst_term_comp, subst_term_id; reflexivity.
    - apply ex_equiv. intros B s HB. destruct s as [n|[]], x as [m|[]].
      assert (B (rm_const_fm [$(S n)..])[$m..] B (rm_const_fm [$(S n)..][t..])).
      { eapply H, (Weak Hx); trivial. now rewrite HA. }
      erewrite subst_comp, subst_ext, subst_comp, (rm_const_fm_subst ($(S n)..)). setoid_rewrite subst_ext at 2.
      rewrite . erewrite rm_const_fm_subst, !subst_comp, subst_ext. reflexivity.
      all: intros [|[]]; cbn; try reflexivity. rewrite subst_term_comp, subst_term_id; reflexivity.
  Qed.


  Lemma ZF_subst sigma :
    map (subst_form ) ZFeq' = ZFeq'.
  Proof.
    reflexivity.
  Qed.


  Lemma ZF_subst' sigma :
    (map (subst_form ) minZFeq') = minZFeq'.
  Proof.
    reflexivity.
  Qed.


  Lemma rm_const_shift_subst A :
    map (subst_form ) (map rm_const_fm A) = map rm_const_fm (map (subst_form ) A).
  Proof.
    erewrite map_map, map_ext, map_map. reflexivity. apply rm_const_fm_shift.
  Qed.


  Lemma rm_const_prv' { p : peirce } B phi :
    B A, B = A ZFeq' ([rm_const_fm | p0 A] minZFeq') rm_const_fm .
  Proof.
    intros H. pattern p, B, . revert p B H. apply prv_ind_full; cbn; intros; subst.
    - apply II. now apply ( (::)).
    - eapply IE; eauto.
    - apply AllI. erewrite map_app, ZF_subst', rm_const_shift_subst. apply . now rewrite map_app, ZF_subst.
    - pose proof (rm_const_tm_prv t). eapply Weak in . apply (ExE ). 2: auto.
      edestruct (nameless_equiv_ex ([rm_const_fm p | p ] minZFeq')) as [x ]. specialize ( eq_refl).
      apply (AllE x) in . apply rm_const_fm_swap with (x:=x); auto. apply (Weak ). auto.
    - pose proof (rm_const_tm_prv t). eapply Weak in . apply (ExE ). 2: auto.
      edestruct (nameless_equiv_ex ([rm_const_fm p | p ] minZFeq')) as [x ]. specialize ( eq_refl).
      apply (ExI x). apply rm_const_fm_swap; auto. apply (Weak ). auto.
    - apply (ExE ( eq_refl)). erewrite map_app, ZF_subst', rm_const_shift_subst, rm_const_fm_shift.
      apply ( (::[p[] | p ])). cbn. now rewrite map_app, ZF_subst.
    - apply Exp. eauto.
    - apply in_app_iff in H as [H|H].
      + apply Ctx. apply in_app_iff. left. now apply in_map.
      + eapply Weak. now apply prv_to_min. auto.
    - apply CI; eauto.
    - eapply CE1; eauto.
    - eapply CE2; eauto.
    - eapply DI1; eauto.
    - eapply DI2; eauto.
    - eapply DE; try now apply .
      + now apply ( (::)).
      + now apply ( (::)).
    - apply Pc.
  Qed.


  Lemma rm_const_prv { p : peirce } A phi :
    (A ZFeq') ((map rm_const_fm A) minZFeq') rm_const_fm .
  Proof.
    intros H. now apply (rm_const_prv' H).
  Qed.


End Deduction.