Library Continuations.FOUnify_cps.deb_term_unif



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.

Predicates that count the different elements of a list:

diffelnb is an inductive definition

The definition of DIFFELNB is recursive.


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

Fixpoint DIFFELNB (l : listv) : natProp :=
  match l return (natProp) with
  | Nilvfun x : nat ⇒ 0 = x :>nat
  | Consv y l1
      fun n : nat
      match n return Prop with
      | OFalse
      | 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 nDIFFELNB 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 ndiffelnb 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 l1IS_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 l1IS_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) : listvlistvProp :=
  | remove_init : remove x Nilv Nilv
  | remove_eq : l l0 : listv, remove x l l0remove x (Consv x l) l0
  | remove_n_eq :
       (l l0 : listv) (x0 : var),
      remove x l l0x x0 :>varremove x (Consv x0 l) (Consv x0 l0).

Fixpoint REMOVE (x : var) (l : listv) {struct l} :
 listvProp :=
  match l return (listvProp) with
  | Nilvfun l1 : listvNilv = l1 :>listv
  | Consv v l1
      fun l2 : listv
      x = v :>var REMOVE x l1 l2
      x v :>var
      match l2 return Prop with
      | NilvFalse
      | Consv w l3v = w :>var REMOVE x l1 l3
      end
  end.


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

Lemma REMOVE_remove :
  (l l0 : listv) (x : var), REMOVE x l l0remove 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 ll = 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) l0REMOVE 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 :>varREMOVE 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) l0x x0 :>varNilv 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 :>varNilv 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 l0IS_IN_LV x0 l0IS_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 :>varIS_IN_LV x0 lIS_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) l0REMOVE x l0 l1¬ IS_IN_LV x lst_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 l0IS_IN_LV x lDIFFELNB 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 n0st_inclv l l0S 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 n0inclv l l0n 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 t1IS_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 xConsv x Nilv
  | C lNilv
  | Root l t0list_var t0
  | ConsArg t1 t2Appv (list_var t1) (list_var t2)
  end.


Goal (t : quasiterm) (x : var), IS_IN x tIS_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 tDIFFELNB (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 t1st_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 tt = 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 xV 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 yIS_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 xIS_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 xIS_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 tV x = f x :>quasiterm.


Definition under (s : quasisubst) (t : quasiterm) : Prop :=
   x y : var, dom s yIS_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) : quasitermProp :=
  | 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 tsub u (ConsArg t v)
  | subConsArgr2 : t v : quasiterm, sub u tsub u (ConsArg v t)
  | subRoot2 : (t : quasiterm) (l : fun_), sub u tsub u (Root l t).


Fixpoint SUP (t : quasiterm) : quasitermProp :=
  match t return (quasitermProp) with
  | V xfun u : quasitermFalse
  | C lfun u : quasitermFalse
  | Root l u1fun u : quasitermu1 = 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 t2SUB t1 t2.
intros; elim H; unfold SUB in |- *; simpl in |- *; auto with v62.
Save sub_SUB.

Goal t1 t2 : quasiterm, SUB t1 t2sub 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 uSUP w vSUP 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 vSUB v wSUB u w.
unfold SUB in |- *; intros; apply trans_SUP with v; auto with v62.
Save trans_SUB.

Goal v u : quasiterm, SUB u vu 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 t2SUB (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 tV x t :>quasitermSUB (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 xV 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 : varSubst 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 : varSubst 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 : varSubst 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 : varSubst 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 : varSubst 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 :>quasitermIS_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 :>quasitermIS_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))) n0S 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 yV y = f y) →
      ( y : var, x = yt = f y) → elem_subst x t f.

Goal
(t : quasiterm) (n : var) (f : quasisubst),
{g : quasisubst | t = g n ( p : nat, n pf p = g p)}.
simple induction n.
intros.
  (fun m : natmatch m return quasiterm with
                  | Ot
                  | S pf m
                  end); split; auto with v62.
simple induction p; auto with v62.
intros; elimtype False; auto with v62.
intros.
elim (H (fun x : natf (S x))); intros g0 h0; elim h0; intros.

 (fun m : natmatch m return quasiterm with
                 | Of 0
                 | S pg0 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 yV y = f y) → ¬ IS_IN x tt = 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 uless_subst f g.