Library Continuations.FOUnify_cps.listv_is_in_lv



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


Inductive listv : Set :=
  | Nilv : listv
  | Consv : varlistvlistv.

Definition BNilv (l : listv) : Prop :=
  match l return Prop with
  | NilvTrue
  | Consv x lFalse
  end.

Definition BConsv (l : listv) : Prop :=
  match l return Prop with
  | NilvFalse
  | Consv x lTrue
  end.

Fixpoint Appv (l0 : listv) : listvlistv :=
  fun l1 : listv
  match l0 return listv with
  | Nilvl1
  | Consv x l2Consv x (Appv l2 l1)
  end.

Definition Headv (x : var) (l : listv) : var :=
  match l return var with
  | Nilvx
  | Consv y _y
  end.

Definition Tailv (l : listv) : listv :=
  match l return listv with
  | NilvNilv
  | Consv _ l1l1
  end.


Inductive is_in_lv (x : var) : listvProp :=
  | is_in_lv_init : l : listv, is_in_lv x (Consv x l)
  | is_in_lv_Consv :
       (l : listv) (x0 : var), is_in_lv x lis_in_lv x (Consv x0 l).

Fixpoint IS_IN_LV (x : var) (l : listv) {struct l} : Prop :=
  match l return Prop with
  | NilvFalse
  | Consv y l2IS_IN_LV x l2 x = y :>var
  end.

Lemma is_in_lv_IS_IN_LV :
  (l : listv) (x : var), is_in_lv x lIS_IN_LV x l.
intros; elim H; simpl in |- *; auto.
Qed.

Lemma IS_IN_LV_is_in_lv :
  (l : listv) (x : var), IS_IN_LV x lis_in_lv x l.
simple induction l; simpl in |- *; intros.
elim H.
elim H0; intros.
apply is_in_lv_Consv; auto.
elim H1; apply is_in_lv_init; auto.
Qed.


Lemma IS_IN_LV_n_eq :
  (x x0 : var) (l : listv),
 IS_IN_LV x (Consv x0 l) → x x0 :>varIS_IN_LV x l.
simple induction l; simpl in |- *; intros.
elim H; intros; auto; elim H0; auto.
elim H0; intros; auto.
Qed.


Lemma IS_IN_LV_Consv_Nilv_eq :
  x x0 : var, IS_IN_LV x (Consv x0 Nilv) → x = x0 :>var.
intros; elim H; intros h; elim h; auto.
Qed.


Lemma IS_IN_LV_decS :
  (x : var) (l : listv), {IS_IN_LV x l} + {¬ IS_IN_LV x l}.
simple induction l; simpl in |- *; intros.
auto.
elim H; intros.
auto.
elim (var_eq_decS x v); intros.
auto.
right; tauto.
Qed.

Lemma IS_IN_LV_decP :
  (x : var) (l : listv), IS_IN_LV x l ¬ IS_IN_LV x l.
intros; elim (IS_IN_LV_decS x l); intros; auto.
Qed.


Lemma IS_IN_LV_Appv1 :
  (l l0 : listv) (x : var), IS_IN_LV x lIS_IN_LV x (Appv l l0).
simple induction l; simpl in |- *; intros.
elim H; auto.
elim H0; intros; auto.
Qed.

Lemma IS_IN_LV_Appv2 :
  (l l0 : listv) (x : var), IS_IN_LV x l0IS_IN_LV x (Appv l l0).
intros l; elim l; simpl in |- *; auto.
Qed.

Lemma IS_IN_LV_Appv_IS_IN_LV :
  (l l0 : listv) (x : var),
 IS_IN_LV x (Appv l l0) → IS_IN_LV x l IS_IN_LV x l0.
simple induction l; simpl in |- *; intros; auto.
elim H0; intros; auto.
elim (H l1 x); auto.
Qed.