Require Import Arith.
Require Import nat_complements.
Require Import nat_term_eq_quasiterm.
Require Import is_in_quasiterm_term_subst.
Require Import listv_is_in_lv.

Inductive diffelnb : listv → nat → Prop :=
  | diffelnb_init : diffelnb Nilv 0
  | diffelnb_Consv_in :
      ∀ (l : listv) (n : nat) (x : var),
      diffelnb l n → IS_IN_LV x l → diffelnb (Consv x l) n
  | diffelnb_Consv_n_in :
      ∀ (l : listv) (n : nat) (x : var),
      diffelnb l n → ¬ IS_IN_LV x l → diffelnb (Consv x l) (S n).

Fixpoint DIFFELNB (l : listv) : nat → Prop :=
  match l return (nat → Prop) with
  | Nilv ⇒ fun x : nat ⇒ 0 = x :>nat
  | Consv y l1 ⇒
      fun n : nat ⇒
      match n return Prop with
      | O ⇒ False
      | S p ⇒
          IS_IN_LV y l1 ∧ DIFFELNB l1 (S p) ∨
          ¬ IS_IN_LV y l1 ∧ DIFFELNB l1 p
      end
  end.


Lemma diffelnb_DIFFELNB :
 ∀ (l : listv) (n : nat), diffelnb l n → DIFFELNB l n.
intros; elim H; simpl in |- *; auto with v62.
intros l0 n0; elim n0; simpl in |- *; auto with v62.
elim l0; simpl in |- *; auto with v62.
Qed.

Lemma DIFFELNB_diffelnb :
 ∀ (l : listv) (n : nat), DIFFELNB l n → diffelnb l n.
simple induction l.
simple induction n; simpl in |- *; intros.
exact diffelnb_init.
discriminate H0.
simple induction n; intros.
elim H0. elim H1; intros h; elim h; intros.
apply diffelnb_Consv_in; auto with v62.
apply diffelnb_Consv_n_in; auto with v62.
Qed.


Lemma DIFFELNBor : ∀ l : listv, {count : nat | DIFFELNB l count}.
simple induction l.
∃ 0; simpl in |- *; auto with v62. intros v y H. elim H; intros.
elim (IS_IN_LV_decS v y); intros.
∃ x. cut (DIFFELNB y x); auto with v62.
elim x; simpl in |- *; auto with v62. cut (IS_IN_LV v y); auto with v62. elim y; simpl in |- *; auto with v62. ∃ (S x); simpl in |- *; auto with v62.
Qed.


Lemma DIFFELNB_O : ∀ l : listv, DIFFELNB l 0 → Nilv = l :>listv.
simple induction l; simpl in |- *; auto with v62.
intros; absurd False; auto with v62.
Qed.

Lemma DIFFELNB_Consv_n_O :
 ∀ (l : listv) (n : nat) (x : var),
 DIFFELNB (Consv x l) n → 0 ≠ n :>nat.
simple induction n.
simpl in |- *; tauto.
intros; discriminate.
Qed.


Inductive inclv (l1 l2 : listv) : Prop :=
    inclv_init :
      (∀ y : var, IS_IN_LV y l1 → IS_IN_LV y l2) → inclv l1 l2.

Inductive st_inclv (l1 l2 : listv) : Prop :=
    st_inclv_init :
      ∀ x : var,
      ¬ IS_IN_LV x l1 →
      IS_IN_LV x l2 →
      (∀ y : var, IS_IN_LV y l1 → IS_IN_LV y l2) → st_inclv l1 l2.

Lemma n_st_inclv_l_Nilv : ∀ l : listv, ¬ st_inclv l Nilv.
intros l; unfold not in |- *; intros h; elim h; auto with v62.
Qed.


Inductive remove (x : var) : listv → listv → Prop :=
  | remove_init : remove x Nilv Nilv
  | remove_eq : ∀ l l0 : listv, remove x l l0 → remove x (Consv x l) l0
  | remove_n_eq :
      ∀ (l l0 : listv) (x0 : var),
      remove x l l0 → x ≠ x0 :>var → remove x (Consv x0 l) (Consv x0 l0).

Fixpoint REMOVE (x : var) (l : listv) {struct l} :
 listv → Prop :=
  match l return (listv → Prop) with
  | Nilv ⇒ fun l1 : listv ⇒ Nilv = l1 :>listv
  | Consv v l1 ⇒
      fun l2 : listv ⇒
      x = v :>var ∧ REMOVE x l1 l2 ∨
      x ≠ v :>var ∧
      match l2 return Prop with
      | Nilv ⇒ False
      | Consv w l3 ⇒ v = w :>var ∧ REMOVE x l1 l3
      end
  end.


Lemma remove_REMOVE :
 ∀ (l l0 : listv) (x : var), remove x l l0 → REMOVE x l l0.
intros; elim H; intros; simpl in |- *; auto with v62.
Qed.

Lemma REMOVE_remove :
 ∀ (l l0 : listv) (x : var), REMOVE x l l0 → remove x l l0.
simple induction l.
intros; elim H; apply remove_init.
simple induction l1.
simpl in |- *; intros.
elim H0; intros h1; elim h1; intros.
elim H1; apply remove_eq; auto with v62.
absurd False; auto with v62.
intros.
elim H1; intros.
elim H2; intros h h0; elim h; apply remove_eq; auto with v62.
elim H2; intros h h0; elim h0; intros h1 h2; elim h1; apply remove_n_eq;
 auto with v62.
Qed.


Lemma REMOVE_n_IS_IN_LV_eq :
 ∀ (l l0 : listv) (x : var),
 REMOVE x l l0 → ¬ IS_IN_LV x l → l = l0 :>listv.
intros l l0 x h; cut (remove x l l0).
2: apply REMOVE_remove; auto with v62.
intros h0; elim h0; auto with v62.
intros; elim H1; simpl in |- *; auto with v62.
simpl in |- *; intros.
elim H0; auto with v62; unfold not in |- *; intros; elim H2; auto with v62.
Qed.


Lemma REMOVE_Consv_eq :
 ∀ (l l0 : listv) (x : var), REMOVE x (Consv x l) l0 → REMOVE x l l0.
intros until x; simpl in |- *; intros.
elim H; intros h; elim h; intros; auto with v62.
absurd (x = x :>var); auto with v62.
Qed.

Lemma REMOVE_Consv_n_eq :
 ∀ (l l0 : listv) (x x0 : var),
 REMOVE x (Consv x0 l) (Consv x0 l0) → x0 ≠ x :>var → REMOVE x l l0.
intros l l0 x x0; simpl in |- *; intros; auto with v62.
elim H; intros h; elim h; intros.
absurd (x0 = x :>var); auto with v62.
elim H2; auto with v62.
Qed.


Lemma sig_REMOVE : ∀ (l : listv) (x : var), {l0 : listv | REMOVE x l l0}.
simple induction l; intros.
∃ Nilv; simpl in |- *; auto with v62.
elim (H x); intros l1 h.
elim (var_eq_decS x v); intros h0.
elim h0; ∃ l1; simpl in |- ×.
intuition.
∃ (Consv v l1); simpl in |- ×.
intuition.
Qed.

Lemma exi_REMOVE :
 ∀ (l : listv) (x : var), ∃ l0 : listv, REMOVE x l l0.
intros; elim (sig_REMOVE l x); intros l0 h; ∃ l0; auto with v62.
Qed.


Lemma Headv_REMOVE_Consv_Nilv :
 ∀ (l l0 : listv) (x x0 : var),
 REMOVE x (Consv x0 l) l0 → x ≠ x0 :>var → Nilv ≠ l0 :>listv.
simple induction l0; intros.
elim H; intros h; elim h; intros.
absurd (x = x0 :>var); auto with v62.
absurd False; auto with v62.
apply Diff with BNilv; auto with v62; simpl in |- *; auto with v62.
Qed.

Lemma REMOVE_Consv_n_eq_Headv :
 ∀ (l l0 : listv) (x x0 : var),
 REMOVE x (Consv x0 l) l0 →
 x ≠ x0 :>var → Nilv ≠ l0 :>listv ∧ x0 = Headv x l0 :>var.
intros; split.
apply Headv_REMOVE_Consv_Nilv with l x x0; auto with v62.
cut (REMOVE x (Consv x0 l) l0).
2: auto with v62.
elim l0.
simpl in |- *; intros h; elim h.
intros h0; elim h0; auto with v62.
intros h0; elim h0; intros; absurd False; auto with v62.
intros; simpl in |- ×.
elim H2; intros.
elim H3; intros.
absurd (x = x0 :>var); auto with v62.
elim H3; intros h1 h2; elim h2; auto with v62.
Qed.


Lemma REMOVE_IS_IN_LV_IS_IN_LV :
 ∀ (l l0 : listv) (x x0 : var),
 REMOVE x l l0 → IS_IN_LV x0 l0 → IS_IN_LV x0 l.
intros l l0 x x0 h; cut (remove x l l0).
2: apply REMOVE_remove; auto with v62.
intro; elim H; simpl in |- *; auto with v62.
intros.
elim H3; intros; auto with v62.
Qed.

Lemma REMOVE_n_eq_IS_IN_LV_IS_IN_LV :
 ∀ (l l0 : listv) (x : var),
 REMOVE x l l0 →
 ∀ x0 : var, x ≠ x0 :>var → IS_IN_LV x0 l → IS_IN_LV x0 l0.
intros l l0 x H; cut (remove x l l0).
2: apply REMOVE_remove; auto with v62.
intro; elim H0; simpl in |- *; auto with v62.
intros.
elim H4; auto with v62.
intros; absurd (x = x0 :>var); auto with v62.
intros.
elim H5; auto with v62.
Qed.


Lemma st_inclv_Consv_REMOVE_n_IS_IN_LV_st_inclv :
 ∀ (l l0 l1 : listv) (x : var),
 st_inclv (Consv x l) l0 → REMOVE x l0 l1 → ¬ IS_IN_LV x l → st_inclv l l1.
intros l l0 l1 x h; elim h.
simpl in |- *; intros.
apply st_inclv_init with x0.
unfold not in |- *; intros; apply H; auto with v62.
cut (x0 ≠ x :>var).
intros; apply (REMOVE_n_eq_IS_IN_LV_IS_IN_LV l0 l1 x); auto with v62.
unfold not in |- *; intros; elim H4; auto with v62.
intros; cut (x ≠ y :>var).
intros; apply (REMOVE_n_eq_IS_IN_LV_IS_IN_LV l0 l1 x); auto with v62.
unfold not in |- *; intros; apply H3; replace x with y; auto with v62.
Qed.


Lemma REMOVE_n_IS_IN_LV_DIFFELNB_pred :
 ∀ (l : listv) (n : nat),
 DIFFELNB l n →
 ∀ (l0 : listv) (x : var),
 REMOVE x l l0 → IS_IN_LV x l → DIFFELNB l0 (pred n).
intros l n h; cut (diffelnb l n).
2: apply DIFFELNB_diffelnb; auto with v62.
intros H; elim H.
simpl in |- *; tauto.
intros until x0; elim (var_eq_decP x x0); intro.
elim H3; intros.
apply H1 with x; auto with v62.
apply REMOVE_Consv_eq; auto with v62.
elim l1.
simpl in |- *; intros.
elimtype False; intuition.
intros v y h0 h1; elim h1; intros.
elim H4; intros; absurd (x = x0 :>var); auto with v62.
elim H4; intros h2 h3; elim h3; intros h4 h5; elim h4.
apply diffelnb_DIFFELNB; apply diffelnb_Consv_in.
apply DIFFELNB_diffelnb; apply (H1 y x0); auto with v62.
elim H5; intros; auto with v62; absurd (x = x0 :>var); auto with v62.
apply REMOVE_n_eq_IS_IN_LV_IS_IN_LV with l0 x0; auto with v62.

intros l0 n0 x H0 H1 H2 l1; elim l1.
intros x0 H3 H4.
elim H3; intros h0; elim h0; intros.
cut (¬ IS_IN_LV x l0).
2: auto with v62.
elim H5; intros; cut (l0 = Nilv :>listv).
2: apply REMOVE_n_IS_IN_LV_eq with x0; auto with v62.
intros; cut (DIFFELNB l0 n0).
2: apply diffelnb_DIFFELNB; auto with v62; replace l0 with Nilv;
    simpl in |- *; auto with v62.
elim H8; simpl in |- *; auto with v62.
elim H6.
intros v l2 H3 x0 H4 H5.
change (DIFFELNB (Consv v l2) n0) in |- ×.
elim H4; intros.
elim H6; intros.
cut (DIFFELNB l0 n0).
2: apply diffelnb_DIFFELNB; auto with v62.
cut (¬ IS_IN_LV x l0).
2: auto with v62.
elim H7; intros; replace (Consv v l2) with l0;
 try apply REMOVE_n_IS_IN_LV_eq with x0; auto with v62.
elim H6; intros h0 h1; elim h1; intros.
elim H5; intros.
cut (DIFFELNB l2 (pred n0)).
2: apply (H1 l2 x0); auto with v62.
cut (DIFFELNB l0 n0).
2: apply diffelnb_DIFFELNB; auto with v62.
pattern n0 in |- *; apply (nat_case n0).
simpl in |- *; intros; absurd (IS_IN_LV x0 l0); auto with v62.
replace l0 with Nilv; try apply DIFFELNB_O; auto with v62.
simpl in |- *; intros.
elim H7; right; split; auto with v62.
unfold not in |- *; intros; elim H2;
 apply (REMOVE_IS_IN_LV_IS_IN_LV l0 l2 x0); auto with v62.
absurd (x0 = x :>var); auto with v62.
Qed.


Lemma DIFFELNB_st_inclv_le_S :
 ∀ (l : listv) (n : nat),
 DIFFELNB l n →
 ∀ (l0 : listv) (n0 : nat), DIFFELNB l0 n0 → st_inclv l l0 → S n ≤ n0.
intros l n hyp; cut (diffelnb l n).
2: apply DIFFELNB_diffelnb; auto with v62.
intros h; elim h.
intros l0 n0; pattern n0 in |- *; apply (nat_case n0).
simpl in |- *; intros.
elim H0; intros; cut (DIFFELNB l0 0); auto with v62.
intros; absurd (IS_IN_LV x l0); auto with v62.
cut (Nilv = l0 :>listv).
intros H5; elim H5; simpl in |- *; auto with v62.
apply DIFFELNB_O; auto with v62.
intros; auto with v62.
intros until n1; pattern n1 in |- *; apply (nat_case n1).
intros h0 h1; elim h1; intros.
absurd (IS_IN_LV x0 l1); auto with v62.
cut (Nilv = l1 :>listv).
intros H5; elim H5; simpl in |- *; auto with v62.
apply DIFFELNB_O; auto with v62.
intros; apply (H0 l1 (S m)); auto with v62.
elim H3; intros.
apply st_inclv_init with x0; auto with v62.
unfold not in |- *; intros; elim H4; simpl in |- *; auto with v62.
intros; apply H6; simpl in |- *; auto with v62.
intros until n1; pattern n1 in |- *; apply (nat_case n1).
intros h0 h1; elim h1; intros.
absurd (IS_IN_LV x0 l1); auto with v62.
cut (Nilv = l1 :>listv).
intros H5; elim H5; simpl in |- *; auto with v62.
apply DIFFELNB_O; auto with v62.
intros; apply le_n_S.
elim (exi_REMOVE l1 x); intros l2 H5.
apply (H0 l2).
replace m with (pred (S m));
 try apply REMOVE_n_IS_IN_LV_DIFFELNB_pred with l1 x;
 auto with v62.
elim H3; intros.
apply (H7 x); simpl in |- *; auto with v62.
apply st_inclv_Consv_REMOVE_n_IS_IN_LV_st_inclv with l1 x; auto with v62.
Qed.


Lemma inclv_le :
 ∀ (l : listv) (n : nat),
 DIFFELNB l n →
 ∀ (l0 : listv) (n0 : nat), DIFFELNB l0 n0 → inclv l l0 → n ≤ n0.
intros l n hyp; cut (diffelnb l n).
2: apply DIFFELNB_diffelnb; auto with v62.
intros h; elim h.
auto with v62. intros.
apply H0 with l1; auto with v62.
apply inclv_init; intros; elim H3; simpl in |- *; auto with v62.
intros until n1; pattern n1 in |- *; apply (nat_case n1).
intros; absurd (IS_IN_LV x l1).
cut (Nilv = l1 :>listv).
2: apply DIFFELNB_O; auto with v62.
intros H4; elim H4; simpl in |- *; auto with v62.
elim H3; simpl in |- *; auto with v62.
intros; elim (exi_REMOVE l1 x); intros.
apply le_n_S; apply H0 with x0.
replace m with (pred (S m)); auto with v62.
apply REMOVE_n_IS_IN_LV_DIFFELNB_pred with l1 x; auto with v62.
elim H3; simpl in |- *; auto with v62.
apply inclv_init; intros.
apply REMOVE_n_eq_IS_IN_LV_IS_IN_LV with l1 x; auto with v62.
unfold not in |- *; intros h0; absurd (IS_IN_LV y l0); auto with v62; elim h0;
 auto with v62.
elim H3; simpl in |- *; auto with v62.
Qed.


Inductive infv (t1 t2 : quasiterm) : Prop :=
    infv_init :
      ∀ x : var,
      ¬ IS_IN x t1 →
      IS_IN x t2 → (∀ y : var, IS_IN y t1 → IS_IN y t2) → infv t1 t2.


Inductive clos (t : quasiterm) : Prop :=
    clos_init : (∀ x : var, ¬ IS_IN x t) → clos t.


Fixpoint list_var (t : quasiterm) : listv :=
  match t return listv with
  | V x ⇒ Consv x Nilv
  | C l ⇒ Nilv
  | Root l t0 ⇒ list_var t0
  | ConsArg t1 t2 ⇒ Appv (list_var t1) (list_var t2)
  end.


Goal ∀ (t : quasiterm) (x : var), IS_IN x t → IS_IN_LV x (list_var t).
simple induction t; simpl in |- *; intros; auto with v62.
elim H1; intros.
apply IS_IN_LV_Appv1; auto with v62.
apply IS_IN_LV_Appv2; auto with v62.
Save IS_IN_IS_IN_LV.

Goal ∀ (t : quasiterm) (x : var), IS_IN_LV x (list_var t) → IS_IN x t.
simple induction t; simpl in |- *; auto with v62.
tauto.
intros q H q0 H0 x H1;
 elim (IS_IN_LV_Appv_IS_IN_LV (list_var q) (list_var q0) x H1);
 intros; auto with v62.
Save IS_IN_LV_IS_IN.

Goal ∀ t : quasiterm, DIFFELNB (list_var t) 0 → clos t.
intros; apply clos_init.
unfold not in |- *; intros x h; absurd (IS_IN_LV x (list_var t)).
replace (list_var t) with Nilv; try apply (DIFFELNB_O (list_var t));
 auto with v62.
apply IS_IN_IS_IN_LV; auto with v62.
Save DIFFELNB_O_clos.


Goal ∀ t1 t2 : quasiterm, clos (ConsArg t1 t2) → clos t1.
intros; elim H; intros; apply clos_init.
intros x; unfold not in |- *; intros; elim (H0 x); simpl in |- *;
 auto with v62.
Save closConsArg1.

Goal ∀ t1 t2 : quasiterm, clos (ConsArg t1 t2) → clos t2.
intros; elim H; intros; apply clos_init.
intros x; unfold not in |- *; intros; elim (H0 x); simpl in |- *;
 auto with v62.
Save closConsArg2.

Goal ∀ t1 t2 : quasiterm, clos (ConsArg t1 t2) → clos t1 ∧ clos t2.
intros; elim H; intros; split; apply clos_init.
intros x; unfold not in |- *; intros; elim (H0 x); simpl in |- *;
 auto with v62.
intros x; unfold not in |- *; intros; elim (H0 x); simpl in |- *;
 auto with v62.
Save closConsArg.

Goal ∀ (f : fun_) (y : quasiterm), clos (Root f y) → clos y.
intros.
elim H.
intros.
apply clos_init.
intros.
generalize (H0 x).
simpl in |- *; auto with v62.
Save closRoot.

Goal ∀ t : quasiterm, clos t → DIFFELNB (list_var t) 0.
simple induction t.
intros; elim H.
simpl in |- *; intros; absurd (v = v :>var); auto with v62.
intros; simpl in |- *; auto with v62.
intros; simpl in |- *; apply H; generalize (closRoot _ _ H0);
 auto with v62.
simpl in |- *; intros q H q0 H0 H1.
elim (closConsArg q q0 H1); intros.
replace (list_var q) with Nilv; try apply DIFFELNB_O; auto with v62.
Save clos_DIFFELNBO.

Goal
∀ t0 t1 : quasiterm, infv t0 t1 → st_inclv (list_var t0) (list_var t1).
intros; elim H; intros.
apply st_inclv_init with x.
unfold not in |- *; intros; elim H0; apply IS_IN_LV_IS_IN; auto with v62.
apply IS_IN_IS_IN_LV; auto with v62.
intros; apply IS_IN_IS_IN_LV; apply H2; apply IS_IN_LV_IS_IN; auto with v62.
Save infv_st_inclv.

Goal
∀ t0 t1 : quasiterm, st_inclv (list_var t0) (list_var t1) → infv t0 t1.
intros; elim H; intros.
apply infv_init with x.
unfold not in |- *; intros; elim H0; apply IS_IN_IS_IN_LV; auto with v62.
apply IS_IN_LV_IS_IN; auto with v62.
intros; apply IS_IN_LV_IS_IN; apply H2; apply IS_IN_IS_IN_LV; auto with v62.
Save st_inclv_infv.

Goal ∀ t : quasiterm, clos t → ∀ t0 : quasiterm, ¬ infv t0 t.
unfold not in |- *; intros.
elim H; intros.
elim H0; intros.
elim (H1 x); auto with v62.
Save n_infv_t_clos.


Goal
∀ (f : quasisubst) (t : quasiterm),
(∀ x : var, V x = f x :>quasiterm) → t = Subst f t :>quasiterm.
simple induction t; simpl in |- *; auto with v62; intros.
elim H; auto with v62.
elim H; elim H0; auto with v62.
Save eq_V_stab.

Goal ∀ t : quasiterm, t = Subst V t :>quasiterm.
intros; apply eq_V_stab; auto with v62.
Save V_stab.

Goal
∀ (t : quasiterm) (f : quasisubst), clos t → t = Subst f t :>quasiterm.
intros; elim H; intros.
apply trans_equal with (Subst V t); try apply V_stab.
apply eq_restriction_s_t; intros; absurd (IS_IN x t); auto with v62.
Save clossubst.


Definition dom (f : quasisubst) (x : var) : Prop := V x ≠ f x :>quasiterm.

Goal ∀ (f : quasisubst) (x : var), ¬ dom f x → V x = f x :>quasiterm.
intros f x; elim (quasiterm_eq_decP (V x) (f x)); intros; auto with v62.
elim H0; auto with v62.
Save n_dom.

Goal ∀ (f : quasisubst) (x : var), dom f x ∨ ¬ dom f x.
intros f x; elim (quasiterm_eq_decP (V x) (f x)); intros; auto with v62.
Save dom_decP.


Inductive range (s : quasisubst) (x : var) : Prop :=
    range_init : ∀ y : var, dom s y → IS_IN x (s y) → range s x.

Goal
∀ (f : quasisubst) (x : var),
¬ range f x → ∀ y : var, dom f y → ¬ IS_IN x (f y).
unfold not in |- *; intros.
elim H; apply range_init with y; auto with v62.
Save n_range_n_IS_IN.

Goal
∀ (f : quasisubst) (x y : var),
¬ range f x → IS_IN x (f y) → x = y :>var.
intros.
elim (dom_decP f y); intros h.
absurd (IS_IN x (f y)); auto with v62.
unfold not in |- *; intros; elim H; intros.
apply range_init with y; auto with v62.
change (IS_IN x (V y)) in |- ×.
replace (V y) with (f y); auto with v62.
elim (n_dom f y); auto with v62.
Save n_range_IS_IN_eq.

Goal
∀ (f : quasisubst) (t : quasiterm) (x : var),
¬ range f x → IS_IN x (Subst f t) → IS_IN x t.
simple induction t; simpl in |- *; intros; auto with v62.
simpl in |- *; intros; apply n_range_IS_IN_eq with f; auto with v62.
elim H2; intros; auto with v62.
Save n_range_IS_IN_Subst.


Definition over (f : quasisubst) (t : quasiterm) : Prop :=
  ∀ x : var, ¬ IS_IN x t → V x = f x :>quasiterm.


Definition under (s : quasisubst) (t : quasiterm) : Prop :=
  ∀ x y : var, dom s y → IS_IN x (s y) → IS_IN x t.


Goal
∀ (f : quasisubst) (t : quasiterm) (x : var),
IS_IN x (Subst f t) → ∃ y : var, IS_IN y t ∧ IS_IN x (f y).
simple induction t; simpl in |- *; intros; auto with v62. ∃ v; auto with v62.
elim H.
elim H1; intros.
elim H with x; intros; auto with v62.
elim H3; intros; ∃ x0; auto with v62.
elim H0 with x; intros; auto with v62.
elim H3; intros; ∃ x0; auto with v62.
Save IS_IN_Subst_exi_IS_IN.

Goal
∀ (f : quasisubst) (t : quasiterm),
under f t → ∀ x : var, IS_IN x (Subst f t) → IS_IN x t.
unfold under in |- *; intros.
elim (IS_IN_Subst_exi_IS_IN f t x H0); intros x0 h; elim h; intros.
elim (var_eq_decP x0 x); intros h0.
elim h0; auto with v62.
apply (H x x0); auto with v62.
unfold dom in |- *; unfold not in |- *; intros.
elim h0; symmetry in |- *; change (IS_IN x (V x0)) in |- ×.
replace (V x0) with (f x0); auto with v62.
Save under_IS_IN_Subst_IS_IN.


Inductive sub (u : quasiterm) : quasiterm → Prop :=
  | subConsArgl : ∀ t : quasiterm, sub u (ConsArg u t)
  | subConsArgr : ∀ t : quasiterm, sub u (ConsArg t u)
  | subRoot : ∀ l : fun_, sub u (Root l u)
  | subConsArgl2 : ∀ t v : quasiterm, sub u t → sub u (ConsArg t v)
  | subConsArgr2 : ∀ t v : quasiterm, sub u t → sub u (ConsArg v t)
  | subRoot2 : ∀ (t : quasiterm) (l : fun_), sub u t → sub u (Root l t).


Fixpoint SUP (t : quasiterm) : quasiterm → Prop :=
  match t return (quasiterm → Prop) with
  | V x ⇒ fun u : quasiterm ⇒ False
  | C l ⇒ fun u : quasiterm ⇒ False
  | Root l u1 ⇒ fun u : quasiterm ⇒ u1 = u :>quasiterm ∨ SUP u1 u
  | ConsArg u1 u2 ⇒
      fun u : quasiterm ⇒
      u1 = u :>quasiterm ∨ u2 = u :>quasiterm ∨ SUP u1 u ∨ SUP u2 u
  end.

Definition SUB (t1 t2 : quasiterm) : Prop := SUP t2 t1.


Goal ∀ t1 t2 : quasiterm, sub t1 t2 → SUB t1 t2.
intros; elim H; unfold SUB in |- *; simpl in |- *; auto with v62.
Save sub_SUB.

Goal ∀ t1 t2 : quasiterm, SUB t1 t2 → sub t1 t2.
simple induction t2; intros.
elim H.
elim H.
elim H0; intros.
elim H1; apply subRoot.
apply subRoot2; auto with v62.
elim H1; intros.
elim H2; apply subConsArgl.
elim H2; intros.
elim H3; apply subConsArgr.
elim H3; intros.
apply subConsArgl2; auto with v62.
apply subConsArgr2; auto with v62.
Save SUB_sub.


Goal ∀ v u w : quasiterm, SUP v u → SUP w v → SUP w u.
simple induction v.
intros; absurd False; auto with v62. intros; absurd False; auto with v62. simple induction w.
intros; absurd False; auto with v62. intros; absurd False; auto with v62. intros.
elim H2; intros; elim H1; intros; simpl in |- *; auto with v62.
elim H4; replace q0 with (Root f q); simpl in |- *; auto with v62.
replace q0 with (Root f q); simpl in |- *; auto with v62.
intros q0 H0 q1 H1 H2 H3.
elim H3; intro H4.
replace q0 with (Root f q); simpl in |- *; auto with v62.
elim H4; intro H5.
replace q1 with (Root f q); simpl in |- *; auto with v62.
elim H5; intros; simpl in |- *; auto with v62.
simple induction w.
tauto. tauto. intros f q1 H1 H2 H3.
elim H3; intros.
replace q1 with (ConsArg q q0); simpl in |- *; auto with v62.
simpl in |- *; auto with v62.
intros q1 H1 q2 H2 H3 H4.
elim H4; intro H5.
elim H3; intro H6.
elim H6; intros; replace q1 with (ConsArg q q0); simpl in |- *; auto with v62.
replace q1 with (ConsArg q q0); simpl in |- *; auto with v62.
elim H5; intro H6.
replace q2 with (ConsArg q q0); simpl in |- *; auto with v62.
elim H6; intros; simpl in |- *; auto with v62.
Save trans_SUP.

Goal ∀ v u w : quasiterm, SUB u v → SUB v w → SUB u w.
unfold SUB in |- *; intros; apply trans_SUP with v; auto with v62.
Save trans_SUB.

Goal ∀ v u : quasiterm, SUB u v → u ≠ v.
intros.
unfold not in |- *; intros h; cut (SUB u v); auto with v62; elim h.
elim u; simpl in |- *; auto with v62. intros.
elim H1; intros.
apply H0; pattern q in |- *; replace q with (Root f q); auto with v62.
apply H0; apply trans_SUB with (Root f q); unfold SUB in |- *; simpl in |- *;
 auto with v62.
intros.
elim H2; intros.
apply H0; pattern q in |- *; replace q with (ConsArg q q0); auto with v62.
elim H3; intros.
apply H1; pattern q0 in |- *; replace q0 with (ConsArg q q0); auto with v62.
elim H4; intros.
apply H0; apply trans_SUB with (ConsArg q q0); unfold SUB in |- *;
 simpl in |- *; auto with v62.
apply H1; apply trans_SUB with (ConsArg q q0); unfold SUB in |- *;
 simpl in |- *; auto with v62.
Save SUB_diff.

Goal
∀ (t1 t2 : quasiterm) (f : quasisubst),
SUB t1 t2 → SUB (Subst f t1) (Subst f t2).
unfold SUB in |- *; simple induction t2; simpl in |- *; intros.
elim H.
elim H.
elim H0; intros h0.
elim h0; auto with v62.
auto with v62.
elim H1; intros h1.
elim h1; auto with v62.
elim h1; intros h2; elim h2; auto with v62.
Save SUB_subst.

Goal
∀ (x : var) (t : quasiterm) (f : quasisubst),
IS_IN x t → V x ≠ t :>quasiterm → SUB (f x) (Subst f t).
intros; change (SUB (Subst f (V x)) (Subst f t)) in |- *; apply SUB_subst.
unfold SUB in |- *; cut (V x ≠ t :>quasiterm); auto with v62;
 cut (IS_IN x t); try apply IS_IN_is_in; auto with v62.
elim t.
simpl in |- *; intros; absurd (V x = V v :>quasiterm); auto with v62.

simpl in |- *; intros; absurd False; auto with v62.
intros; elim (quasiterm_eq_decP (V x) q); intros.
elim H4; simpl in |- *; auto with v62.
cut (IS_IN x (Root f0 q)); simpl in |- *; auto with v62.
simpl in |- *; intros.
elim (quasiterm_eq_decP (V x) q); intros; auto with v62.
elim (quasiterm_eq_decP (V x) q0); intros; auto with v62.
elim H3; intros; auto with v62.
Save IS_IN_SUB.


Definition idempotent (s : quasisubst) : Prop :=
  ∀ x : var, s x = Subst s (s x).


Goal
∀ f : quasisubst,
(∀ x : var, range f x → V x = f x :>quasiterm) → idempotent f.
unfold idempotent in |- *; intros.
elim (quasiterm_eq_decP (V x) (f x)); intros h.
elim h; auto with v62.
apply trans_equal with (Subst V (f x)).
apply V_stab.
apply eq_restriction_s_t.
intros; apply H; apply range_init with x; auto with v62.
Save range_n_dom_idempotent.


Goal
∀ f : quasisubst, idempotent f → ∀ x : var, dom f x → ¬ range f x.
unfold not in |- *; intros.
elim H0; elim H1; intros.
apply (eq_restriction_t_s (f y) V f); auto with v62.
elim H; elim V_stab with (f y); auto with v62.
Save idempotent_n_range.


Goal
∀ f : quasisubst,
idempotent f → ∀ x : var, dom f x → ∀ y : var, ¬ IS_IN x (f y).
intros.
elim (dom_decP f y); intros.
apply n_range_n_IS_IN; auto with v62.
apply idempotent_n_range; auto with v62.
elim (n_dom f y H1); simpl in |- ×.
unfold not in |- *; intros h; absurd (dom f y); auto with v62; elim h;
 auto with v62.
Save idempotent_dom_n_IS_IN.


Goal
∀ (t : quasiterm) (f g : quasisubst),
idempotent f →
idempotent g →
under g (Subst f t) →
over g (Subst f t) → idempotent (fun x : var ⇒ Subst g (f x)).
unfold under in |- *; unfold over in |- *; intros;
 apply range_n_dom_idempotent; intros.
elim H3; intros.
elim (dom_decP g x); intros.
absurd (IS_IN x (Subst g (f y))); auto with v62.
apply n_IS_IN_Subst.
intros; apply idempotent_dom_n_IS_IN; auto with v62.
elim (dom_decP f x); intros.
absurd (IS_IN x (f y)).
apply idempotent_dom_n_IS_IN; auto with v62.
apply (n_range_IS_IN_Subst g (f y)); auto with v62.
unfold not in |- *; intros H8; elim H8; intros.
absurd (IS_IN x (Subst f t)).
apply n_IS_IN_Subst.
intros; apply idempotent_dom_n_IS_IN; auto with v62.
apply (H1 x y0); auto with v62.
elim (n_dom f x H7); simpl in |- *; elim (n_dom g x H6); simpl in |- *;
 auto with v62.
Save idempotent_Fondamental.


Goal
∀ (f g : quasisubst) (t : quasiterm),
Subst g (Subst f t) = Subst (fun x : var ⇒ Subst g (f x)) t.
simple induction t; simpl in |- *; intros; auto with v62.
elim H; auto with v62.
elim H; elim H0; auto with v62.
Save comp_subst.

Goal
∀ (f g : quasisubst) (t : quasiterm),
Subst (fun x : var ⇒ Subst g (f x)) t = Subst g (Subst f t).
intros; symmetry in |- *; apply comp_subst.
Save exp_comp_subst.


Goal
∀ (p1 p2 p3 p4 : quasiterm) (f g : quasisubst),
over f (ConsArg p1 p2) →
over g (ConsArg (Subst f p3) (Subst f p4)) →
under f (ConsArg p1 p2) →
over (fun x : var ⇒ Subst g (f x)) (ConsArg (ConsArg p1 p3) (ConsArg p2 p4)).
unfold over, under in |- *; intros.
cut (¬ IS_IN x (ConsArg p1 p2)).
intros h; elim (H x h).
simpl in |- *; apply H0; unfold not in |- *; intros; elim H2.


apply n_range_IS_IN_Subst with f.
unfold not in |- *; intros h0; elim h0; intros.
elim h; apply H1 with y; auto with v62.
simpl in |- *; elim H3; auto with v62.
simpl in |- *; unfold not in |- *; intros h; elim H2; simpl in |- *; elim h;
 intros; auto with v62.
Save over_comp.


Goal
∀ (p1 p2 p3 p4 : quasiterm) (f g : quasisubst),
under f (ConsArg p1 p2) →
under g (ConsArg (Subst f p3) (Subst f p4)) →
over f (ConsArg p1 p2) →
over g (ConsArg (Subst f p3) (Subst f p4)) →
under (fun x : var ⇒ Subst g (f x))
  (ConsArg (ConsArg p1 p3) (ConsArg p2 p4)).
unfold over, dom, under in |- *; intros.


apply under_IS_IN_Subst_IS_IN with g.
unfold under, over, dom in |- *; intros.
cut (IS_IN x0 (Subst f (ConsArg p3 p4))).
intros H7; elim (IS_IN_Subst_exi_IS_IN f (ConsArg p3 p4) x0 H7); intros.
elim H8; intros h1 h2.
apply under_IS_IN_Subst_IS_IN with f.
unfold under in |- *; intros.
elim H with x2 y1; simpl in |- *; auto with v62.
elim (H0 x0 y0); simpl in |- *; auto with v62.
elim (H0 x0 y0); simpl in |- *; auto with v62.
elim (IS_IN_Subst_exi_IS_IN g (f y) x H4); intros.
elim H5; intros.
apply IS_IN_Subst_IS_IN with x0; auto with v62.
elim (dom_decP f y); intros.
elim (H x0 y); simpl in |- *; auto with v62.
cut (IS_IN x0 (f y)); auto with v62; elim (n_dom f y H8); intros.
elim (dom_decP g x0); intros.
elim (IS_IN_decP x0 (ConsArg (Subst f p3) (Subst f p4))); intros h.
elim (IS_IN_Subst_exi_IS_IN f (ConsArg p3 p4) x0 h); intros x1 h1; elim h1;
 intros.
elim (dom_decP f x1); intros.
elim H with x0 x1; simpl in |- *; auto with v62.
cut (IS_IN x0 (f x1)); auto with v62; elim (n_dom f x1 H13); intros.
cut (IS_IN x1 (ConsArg p3 p4)); auto with v62; elim H14.
simpl in |- *; intros h2; elim h2; intros; auto with v62.
absurd (V x0 = g x0 :>quasiterm); auto with v62.
absurd (V y = Subst g (f y) :>quasiterm); auto with v62.
elim (n_dom f y H8); simpl in |- *; elim H9; elim (n_dom g x0 H10);
 auto with v62.
Save under_comp.


Goal
∀ (t : quasiterm) (f : quasisubst),
over f t → (∃ x : var, V x ≠ f x) ∨ (∀ v : var, V v = f v).
cut
 (∀ (l : listv) (f : quasisubst),
  (∀ x : var, V x ≠ f x :>quasiterm → IS_IN_LV x l) →
  (∃ x : var, V x ≠ f x :>quasiterm) ∨
  (∀ v : var, V v = f v :>quasiterm)).
unfold over in |- *; intros.
apply H with (list_var t); intros.
apply IS_IN_IS_IN_LV.
elim (IS_IN_decP x t); intros; auto with v62.
absurd (V x = f x :>quasiterm); auto with v62.
simple induction l; simpl in |- *; intros.
right; intros.
elim (quasiterm_eq_decP (V v) (f v)); intros; auto with v62.
elim (H v H0).
elim (quasiterm_eq_decP (V v) (f v)); intros.
apply (H f); intros.
elim (H0 x H2); intros; auto with v62.
absurd (V v = f v :>quasiterm); auto with v62; elim H3; auto with v62.
left; ∃ v; auto with v62.
Save ident_or_not.

Goal
∀ (t : quasiterm) (f : quasisubst),
over f t →
{x : var | V x ≠ f x :>quasiterm} +
{(∀ x : var, V x = f x :>quasiterm)}.
cut
 (∀ (l : listv) (f : quasisubst),
  (∀ x : var, V x ≠ f x :>quasiterm → IS_IN_LV x l) →
  {x : var | V x ≠ f x :>quasiterm} +
  {(∀ x : var, V x = f x :>quasiterm)}).
unfold over in |- *; intros.
apply H with (list_var t); intros.
apply IS_IN_IS_IN_LV.
elim (IS_IN_decP x t); intros; auto with v62.
absurd (V x = f x :>quasiterm); auto with v62.
simple induction l; simpl in |- *; intros.
right; intros.
elim (quasiterm_eq_decP (V x) (f x)); intros; auto with v62.
elim (H x H0).
elim (quasiterm_eq_decS (V v) (f v)); intros.
apply (H f); intros.
elim (H0 x H1); intros; auto with v62.
absurd (V v = f v :>quasiterm); auto with v62; elim H2; auto with v62.
left; ∃ v; auto with v62.
Save ident_or_notS.


Goal
∀ (t1 t2 t3 t4 : quasiterm) (n : nat),
DIFFELNB (list_var (ConsArg (ConsArg t1 t2) (ConsArg t3 t4))) n →
∀ f : quasisubst,
idempotent f →
over f (ConsArg t1 t3) →
under f (ConsArg t1 t3) →
(∃ x : var, V x ≠ f x :>quasiterm) →
∀ n0 : nat,
DIFFELNB (list_var (ConsArg (Subst f t2) (Subst f t4))) n0 → S n0 ≤ n.
unfold over, under in |- *; intros.
elim H3; intros.
apply
 DIFFELNB_st_inclv_le_S
  with
    (list_var (ConsArg (Subst f t2) (Subst f t4)))
    (list_var (ConsArg (ConsArg t1 t2) (ConsArg t3 t4)));
 auto with v62.
apply st_inclv_init with x.
change (¬ IS_IN_LV x (list_var (Subst f (ConsArg t2 t4)))) in |- ×.
unfold not in |- *; intros; cut (IS_IN x (Subst f (ConsArg t2 t4))); intros.
2: apply IS_IN_LV_IS_IN; auto with v62.
elim (IS_IN_Subst_exi_IS_IN f (ConsArg t2 t4) x H7); intros.
elim H8; intros.
absurd (IS_IN x (f x0)); auto with v62; apply idempotent_dom_n_IS_IN;
 auto with v62.
apply IS_IN_IS_IN_LV; elim (IS_IN_decP x (ConsArg t1 t3)); intros.
cut (IS_IN x (ConsArg t1 t3)).
2: auto with v62.
simpl in |- *; intros h; elim h; auto with v62.
absurd (V x = f x :>quasiterm); auto with v62.
intros; cut (IS_IN y (Subst f (ConsArg t2 t4))).
2: apply IS_IN_LV_IS_IN; auto with v62.
intros; apply IS_IN_IS_IN_LV;
 elim (IS_IN_Subst_exi_IS_IN f (ConsArg t2 t4) y H7);
 intros.
elim H8; intros.
elim (dom_decP f x0); intros.
cut (IS_IN y (ConsArg t1 t3)).
2: apply (H2 y x0); auto with v62.
simpl in |- *; intros h; elim h; auto with v62.
cut (V x0 = f x0 :>quasiterm).
2: apply n_dom; auto with v62.
intros; cut (y = x0 :>var).
intros h; cut (IS_IN x0 (ConsArg t2 t4)).
2: auto with v62.
elim h; simpl in |- *; intros h1; elim h1; auto with v62.
cut (IS_IN y (f x0)); auto with v62; elim H12; simpl in |- *; auto with v62.
Save f_n_id_minus.


Inductive elem_subst (x : var) (t : quasiterm) (f : quasisubst) : Prop :=
    elem_subst_init :
      (∀ y : var, x ≠ y → V y = f y) →
      (∀ y : var, x = y → t = f y) → elem_subst x t f.

Goal
∀ (t : quasiterm) (n : var) (f : quasisubst),
{g : quasisubst | t = g n ∧ (∀ p : nat, n ≠ p → f p = g p)}.
simple induction n.
intros. ∃
  (fun m : nat ⇒ match m return quasiterm with
                  | O ⇒ t
                  | S p ⇒ f m
                  end); split; auto with v62.
simple induction p; auto with v62.
intros; elimtype False; auto with v62.
intros.
elim (H (fun x : nat ⇒ f (S x))); intros g0 h0; elim h0; intros.
∃
 (fun m : nat ⇒ match m return quasiterm with
                 | O ⇒ f 0
                 | S p ⇒ g0 p
                 end); split; auto with v62.
simple induction p; auto with v62.
Save sig_elem_subst0.

Goal ∀ (x : var) (t : quasiterm), {f : quasisubst | elem_subst x t f}.
intros; elim (sig_elem_subst0 t x V); intros.
∃ x0; elim p; intros; apply elem_subst_init; auto with v62.
intros y0 h; elim h; auto with v62.
Save sig_elem_subst.

Goal
∀ (t : quasiterm) (x : var) (f : quasisubst),
(∀ y : var, x ≠ y → V y = f y) → ¬ IS_IN x t → t = Subst f t.
intros.
replace (Subst f t) with (Subst V t); try apply V_stab.
apply eq_restriction_s_t.
intros; elim (var_eq_decP x x0); intros; auto with v62.
absurd (IS_IN x0 t); auto with v62; elim H2; auto with v62.
Save elem_subst_conserve.


Inductive less_subst (f g : quasisubst) : Prop :=
    less_subst_init :
      ∀ h : quasisubst,
      (∀ x : var, Subst h (f x) = g x) → less_subst f g.


Definition unif (f : quasisubst) (t u : quasiterm) : Prop :=
  Subst f t = Subst f u.


Definition min_unif (f : quasisubst) (t u : quasiterm) : Prop :=
  ∀ g : quasisubst, unif g t u → less_subst f g.