From: Wilmer Ricciotti <ricciott@cs.unibo.it>
Date: Fri, 19 Jun 2009 14:53:57 +0000 (+0000)
Subject: More improvements.
X-Git-Tag: make_still_working~3835
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=92057ea600a468c1d0379f046921d551a7f37e55;p=helm.git

More improvements.
---

diff --git a/helm/software/matita/contribs/POPLmark/Fsub/adeq.ma b/helm/software/matita/contribs/POPLmark/Fsub/adeq.ma
index 056a5105b..d4fdeca81 100644
--- a/helm/software/matita/contribs/POPLmark/Fsub/adeq.ma
+++ b/helm/software/matita/contribs/POPLmark/Fsub/adeq.ma
@@ -1,4 +1,3 @@
-
 (**************************************************************************)
 (*       ___                                                              *)
 (*      ||M||                                                             *)
@@ -27,58 +26,15 @@ record nbound : Set \def {
                            nbtype : NTyp
                          }.
 
-inductive option (A:Type) : Set \def
-| Some : A \to option A
-| None : option A.
-
-definition swap : nat → nat → nat → nat ≝
-  λu,v,x.match (eqb x u) with
-    [true ⇒ v
-    |false ⇒ match (eqb x v) with
-       [true ⇒ u
-       |false ⇒ x]].
-       
-lemma swap_left : ∀x,y.(swap x y x) = y.
-intros;unfold swap;rewrite > eqb_n_n;simplify;reflexivity;
-qed.
-
-lemma swap_right : ∀x,y.(swap x y y) = x.
-intros;unfold swap;rewrite > eqb_n_n;apply (eqb_elim y x);intro;autobatch;
-qed.
-
-lemma swap_other : \forall x,y,z.(z \neq x) \to (z \neq y) \to (swap x y z) = z.
-intros;unfold swap;apply (eqb_elim z x);intro;simplify
-  [elim H;assumption
-  |rewrite > not_eq_to_eqb_false;autobatch]
-qed.
-
-lemma swap_inv : \forall u,v,x.(swap u v (swap u v x)) = x.
-intros;unfold in match (swap u v x);apply (eqb_elim x u);intro;simplify
-  [autobatch paramodulation
-  |apply (eqb_elim x v);intro;simplify
-     [autobatch paramodulation
-     |apply swap_other;assumption]]
-qed.
-
-lemma swap_inj : ∀u,v,x,y.swap u v x = swap u v y → x = y.
-intros 4;unfold swap;apply (eqb_elim x u);simplify;intro
-  [apply (eqb_elim y u);simplify;intro
-     [intro;autobatch paramodulation
-     |apply (eqb_elim y v);simplify;intros
-        [autobatch paramodulation
-        |elim H2;symmetry;assumption]]
-  |apply (eqb_elim y u);simplify;intro
-     [apply (eqb_elim x v);simplify;intros;
-        [autobatch paramodulation
-        |elim H2;assumption]
-     |apply (eqb_elim x v);simplify;intro
-        [apply (eqb_elim y v);simplify;intros
-           [autobatch paramodulation
-           |elim H1;symmetry;assumption]
-        |apply (eqb_elim y v);simplify;intros
-           [elim H;assumption
-           |assumption]]]]
-qed.
+let rec encodetype T vars on T ≝
+  match T with
+  [ (TName n) ⇒ match (lookup n vars) with
+    [ true ⇒ (TVar (posn vars n))
+    | false ⇒ (TFree n)]
+  | NTop ⇒ Top
+  | (NArrow T1 T2) ⇒ Arrow (encodetype T1 vars) (encodetype T2 vars)
+  | (NForall n2 T1 T2) ⇒ Forall (encodetype T1 vars) 
+                                (encodetype T2 (n2::vars))].
 
 let rec swap_NTyp u v T on T ≝
   match T with
@@ -96,9 +52,6 @@ let rec swap_Typ u v T on T \def
      |(Arrow T1 T2) ⇒ (Arrow (swap_Typ u v T1) (swap_Typ u v T2))
      |(Forall T1 T2) ⇒ (Forall (swap_Typ u v T1) (swap_Typ u v T2))].
                   
-definition swap_list : nat \to nat \to (list nat) \to (list nat) ≝
-  \lambda u,v,l.(map ? ? (swap u v) l). 
- 
 let rec var_NTyp (T:NTyp):list nat\def 
   match T with 
   [TName x ⇒ [x]
@@ -106,84 +59,6 @@ let rec var_NTyp (T:NTyp):list nat\def
   |NArrow U V ⇒ (var_NTyp U)@(var_NTyp V)
   |NForall X U V ⇒ X::(var_NTyp U)@(var_NTyp V)].
 
-inductive alpha_eq : NTyp \to NTyp \to Prop \def
-| A_refl : \forall T.(alpha_eq T T)
-| A_arrow : \forall T1,T2,U1,U2.(alpha_eq T1 U1) \to (alpha_eq T2 U2) \to
-                                (alpha_eq (NArrow T1 T2) (NArrow U1 U2))
-| A_forall : \forall T1,T2,U1,U2,X,Y.
-             (alpha_eq T1 U1) \to 
-             (\forall Z.
-                 \lnot (in_list nat Z (X::Y::((var_NTyp T2)@(var_NTyp U2))))
-                 \to (alpha_eq (swap_NTyp Z X T2) (swap_NTyp Z Y U2))) \to
-             (alpha_eq (NForall X T1 T2) (NForall Y U1 U2)).
-
-let rec posn l x on l ≝
-  match l with
-  [ nil ⇒ O
-  | (cons (y:nat) l2) ⇒
-      match (eqb x y) with
-            [ true ⇒ O
-            | false ⇒ S (posn l2 x)]].
-            
-let rec length A l on l ≝
-  match l with
-    [ nil ⇒ O
-    | (cons (y:A) l2) ⇒ S (length A l2)].
-    
-let rec lookup n l on l ≝
-  match l with
-    [ nil ⇒ false
-    | cons (x:nat) l1 ⇒ match (eqb n x) with
-              [true ⇒ true
-              |false ⇒ (lookup n l1)]]. 
-                             
-let rec encodetype T vars on T ≝
-  match T with
-  [ (TName n) ⇒ match (lookup n vars) with
-    [ true ⇒ (TVar (posn vars n))
-    | false ⇒ (TFree n)]
-  | NTop ⇒ Top
-  | (NArrow T1 T2) ⇒ Arrow (encodetype T1 vars) (encodetype T2 vars)
-  | (NForall n2 T1 T2) ⇒ Forall (encodetype T1 vars) 
-                                (encodetype T2 (n2::vars))].
-
-let rec head (A:Type) l on l ≝
-  match l with
-  [ nil ⇒ None A
-  | (cons (x:A) l2) ⇒ Some A x].
-
-let rec nth n l on n ≝
-  match n with
-  [ O ⇒ match l with
-    [ nil ⇒ O
-    | (cons x l2) ⇒ x]
-  | (S n2) ⇒ (nth n2 (tail ? l))]. 
-
-definition max_list : (list nat) \to nat \def
-  \lambda l.let rec aux l0 m on l0 \def
-    match l0 with
-      [ nil ⇒ m
-      | (cons n l2) ⇒ (aux l2 (max m n))]
-    in aux l O.
-
-let rec decodetype T vars C on T \def
-  match T with
-  [ TVar n ⇒ TName (nth n vars)
-  | TFree x  ⇒ TName x
-  | Top ⇒ NTop
-  | Arrow T1 T2 ⇒ NArrow (decodetype T1 vars C) (decodetype T2 vars C)
-  | Forall T1 T2 ⇒ NForall (S (max_list (vars@C))) (decodetype T1 vars C) 
-       (decodetype T2 ((S (max_list (vars@C)))::vars) C)].
-       
-definition sublist: \forall A:Type.(list A) \to (list A) \to Prop \def
-  \lambda A,l1,l2.\forall x.(in_list ? x l1) \to (in_list ? x l2).
-  
-let rec remove_nat (x:nat) (l:list nat) on l \def
-  match l with
-  [ nil ⇒ (nil nat) 
-  | (cons y l2) ⇒ match (eqb x y) with
-                  [ true ⇒ (remove_nat x l2)
-                  | false ⇒ (y :: (remove_nat x l2)) ]].
 
 let rec fv_NTyp (T:NTyp):list nat\def 
   match T with 
@@ -205,56 +80,55 @@ let rec subst_NTyp_var T X Y \def
                    | false ⇒ (NForall Z (subst_NTyp_var U X Y) 
                                         (subst_NTyp_var V X Y))]].
 
+definition filter_ntypes : list nbound → list nbound ≝
+  λG.(filter ? G (λB.match B with [mk_nbound B X T ⇒ B])).
+
 definition fv_Nenv : list nbound → list nat ≝
-  map nbound nat
+  λG.map nbound nat
     (λb.match b with 
-      [mk_nbound (B:bool) (X:nat) (T:NTyp) ⇒ X]).
+      [mk_nbound (B:bool) (X:nat) (T:NTyp) ⇒ X]) (filter_ntypes G).
           
 inductive NWFType : (list nbound) → NTyp → Prop ≝
-  | NWFT_TName : ∀X,G.(in_list ? X (fv_Nenv G))
+  | NWFT_TName : ∀X,G.(X ∈ (fv_Nenv G))
                 → (NWFType G (TName X))
   | NWFT_Top : ∀G.(NWFType G NTop)
   | NWFT_Arrow : ∀G,T,U.(NWFType G T) → (NWFType G U) →
                 (NWFType G (NArrow T U))
   | NWFT_Forall : ∀G,X,T,U.(NWFType G T) →
-                  (∀Y.¬(in_list ? Y (fv_Nenv G)) →
-                       (Y = X ∨ ¬(in_list ? Y (fv_NTyp U))) → 
+                  (∀Y.Y ∉ (fv_Nenv G) →
+                       (Y = X ∨ Y ∉ (fv_NTyp U)) → 
                     (NWFType ((mk_nbound true Y T) :: G) (swap_NTyp Y X U))) →
                  (NWFType G (NForall X T U)).
 
 inductive NWFEnv : (list nbound) → Prop ≝
   | NWFE_Empty : (NWFEnv (nil ?))
   | NWFE_cons : ∀B,X,T,G.(NWFEnv G) →
-                  ¬(in_list ? X (fv_Nenv G)) → 
+                  X ∉ (fv_Nenv G) → 
                   (NWFType G T) → (NWFEnv ((mk_nbound B X T) :: G)).
           
 inductive NJSubtype : (list nbound) → NTyp → NTyp → Prop ≝
   | NSA_Top : ∀G,T.(NWFEnv G) → (NWFType G T) → (NJSubtype G T NTop)
   | NSA_Refl_TVar : ∀G,X.(NWFEnv G)
-                   → (in_list ? X (fv_Nenv G))
+                   → X ∈ (fv_Nenv G)
                    → (NJSubtype G (TName X) (TName X))
   | NSA_Trans_TVar : ∀G,X,T,U.
-                     (in_list ? (mk_nbound true X U) G) →
+                     (mk_nbound true X U) ∈ G →
                      (NJSubtype G U T) → (NJSubtype G (TName X) T)
   | NSA_Arrow : ∀G,S1,S2,T1,T2.
                (NJSubtype G T1 S1) → (NJSubtype G S2 T2) →
                (NJSubtype G (NArrow S1 S2) (NArrow T1 T2))
   | NSA_All : ∀G,X,Y,S1,S2,T1,T2.
-              (NWFType G (NForall X S1 S2)) \to
-              (NWFType G (NForall Y T1 T2)) \to
+              (NWFType G (NForall X S1 S2)) →
+              (NWFType G (NForall Y T1 T2)) →
               (NJSubtype G T1 S1) →
-              (∀Z.¬(in_list ? Z (fv_Nenv G)) →
-                  (Z = X \lor \lnot in_list ? Z (fv_NTyp S2)) \to
-                  (Z = Y \lor \lnot in_list ? Z (fv_NTyp T2)) \to
+              (∀Z.Z ∉ (fv_Nenv G) →
+                  (Z = X ∨ Z ∉ (fv_NTyp S2)) →
+                  (Z = Y ∨ Z ∉ (fv_NTyp T2)) →
               (NJSubtype ((mk_nbound true Z T1) :: G) 
                     (swap_NTyp Z X S2) (swap_NTyp Z Y T2))) →  
-              (NJSubtype G (NForall X S1 S2) (NForall Y T1 T2))
-  | NSA_alpha : ∀G,T1,T2,U1,U2.(NJSubtype G T1 U1) → 
-                                (alpha_eq T1 T2) →
-                                (alpha_eq U1 U2) →
-                                (NJSubtype G T2 U2).
+              (NJSubtype G (NForall X S1 S2) (NForall Y T1 T2)).
                                 
-let rec nt_len T \def
+let rec nt_len T ≝
   match T with
   [ TName X ⇒ O
   | NTop ⇒ O
@@ -269,7 +143,7 @@ definition encodeenv : list nbound → list bound ≝
 lemma eq_fv_Nenv_fv_env : ∀G. fv_Nenv G = fv_env (encodeenv G).
 intro;elim G;simplify
   [reflexivity
-  |rewrite < H;elim a;simplify;reflexivity]
+  |elim a;elim b;simplify;rewrite < H;reflexivity]
 qed.
 
 lemma decidable_eq_Typ : ∀T,U:Typ.decidable (T = U).
@@ -313,8 +187,8 @@ intros;cases b;cases c;cases (bool_to_decidable_eq b1 b2)
 |right;intro;destruct H1;elim H;reflexivity]
 qed.
 
-lemma in_Nenv_to_in_env: ∀l,n,n2.in_list ? (mk_nbound true n n2) l → 
-                 in_list ? (mk_bound true n (encodetype n2 [])) (encodeenv l).
+lemma in_Nenv_to_in_env: ∀l,n,n2.(mk_nbound true n n2) ∈ l → 
+                 (mk_bound true n (encodetype n2 [])) ∈ (encodeenv l).
 intros 3;elim l
   [elim (not_in_list_nil ? ? H)
   |inversion H1;intros;destruct;
@@ -322,46 +196,6 @@ intros 3;elim l
      |elim a;simplify;apply in_list_cons;apply H;assumption]]
 qed.
                  
-lemma in_lookup : \forall x,l.(in_list ? x l) \to (lookup x l = true).
-intros;elim H;simplify
-  [rewrite > eqb_n_n;reflexivity
-  |rewrite > H2;elim (eqb a a1);reflexivity]
-qed.
-
-lemma lookup_in : \forall x,l.(lookup x l = true) \to (in_list ? x l).
-intros 2;elim l
-  [simplify in H;destruct H
-  |generalize in match H1;simplify;elim (decidable_eq_nat x a)
-     [applyS in_list_head
-     |apply in_list_cons;apply H;
-      rewrite > (not_eq_to_eqb_false ? ? H2) in H3;simplify in H3;assumption]]
-qed.
-
-lemma posn_length : \forall x,vars.(in_list ? x vars) \to 
-                       (posn vars x) < (length ? vars).
-intros 2;elim vars
-  [elim (not_in_list_nil ? ? H)
-  |inversion H1;intros;destruct;simplify
-     [rewrite > eqb_n_n;simplify;
-      apply lt_O_S
-     |elim (eqb x a);simplify
-        [apply lt_O_S
-        |apply le_S_S;apply H;assumption]]]
-qed.
-
-lemma in_remove : \forall a,b,l.(a \neq b) \to (in_list ? a l) \to
-                                (in_list ? a (remove_nat b l)).
-intros 4;elim l
-  [elim (not_in_list_nil ? ? H1)
-  |inversion H2;intros;destruct;simplify
-     [rewrite > not_eq_to_eqb_false
-        [simplify;apply in_list_head
-        |intro;apply H;symmetry;assumption]
-     |elim (eqb b a1);simplify
-        [apply H1;assumption
-        |apply in_list_cons;apply H1;assumption]]]
-qed.
-
 lemma NTyp_len_ind : \forall P:NTyp \to Prop.
                        (\forall U.(\forall V.((nt_len V) < (nt_len U)) \to (P V))
                            \to (P U))
@@ -424,30 +258,15 @@ intros;elim T;simplify
 |*:autobatch paramodulation]
 qed.
 
-lemma swap_same : \forall x,y.swap x x y = y.
-intros;elim (decidable_eq_nat y x)
-  [autobatch paramodulation
-  |rewrite > swap_other;autobatch]
-qed.
-
-lemma not_nat_in_to_lookup_false : ∀l,X.¬(in_list ? X l) → lookup X l = false.
-intros 2;elim l;simplify
-  [reflexivity
-  |elim (decidable_eq_nat X a)
-     [elim H1;rewrite > H2;apply in_list_head
-     |rewrite > (not_eq_to_eqb_false ? ? H2);simplify;apply H;intro;apply H1;
-      apply (in_list_cons ? ? ? ? H3);]]
-qed.
-
 lemma fv_encode : ∀T,l1,l2.
-                  (∀x.(in_list ? x (fv_NTyp T)) →
+                  (∀x.x ∈ (fv_NTyp T) →
                      (lookup x l1 = lookup x l2 ∧
                      (lookup x l1 = true → posn l1 x = posn l2 x))) →
                   (encodetype T l1 = encodetype T l2).
 intro;elim T
   [simplify in H;elim (H n)
-     [simplify;rewrite < H1;generalize in match H2;elim (lookup n l1);simplify
-        [rewrite > H3;autobatch
+     [simplify;rewrite < H1;elim (lookup n l1) in H2;simplify
+        [rewrite > H2;autobatch
         |reflexivity]
      |apply in_list_head]
   |simplify;reflexivity
@@ -473,64 +292,9 @@ intro;elim T
      |intros;apply H2;simplify;apply in_list_to_in_list_append_l;autobatch]]
 qed.
 
-lemma lookup_swap : ∀a,b,x,vars.
-                    lookup (swap a b x) (swap_list a b vars) =
-                    lookup x vars.
-intros 4;elim vars;simplify
-  [reflexivity
-  |elim (decidable_eq_nat x a1)
-     [rewrite > H1;rewrite > eqb_n_n;rewrite > eqb_n_n;simplify;reflexivity
-     |rewrite > (not_eq_to_eqb_false ? ? H1);elim (decidable_eq_nat x a)
-        [rewrite > H;rewrite > H2;rewrite > swap_left;
-         elim (decidable_eq_nat b a1)
-           [rewrite < H3;rewrite > swap_right;
-            rewrite > (not_eq_to_eqb_false b a)
-              [reflexivity
-              |intro;autobatch]
-           |rewrite > (swap_other a b a1)
-              [rewrite > (not_eq_to_eqb_false ? ? H3);simplify;reflexivity
-              |*:intro;autobatch]]
-        |elim (decidable_eq_nat x b)
-           [rewrite > H;rewrite > H3;rewrite > swap_right;
-            elim (decidable_eq_nat a1 a)
-              [rewrite > H4;rewrite > swap_left;
-               rewrite > (not_eq_to_eqb_false a b)
-                 [reflexivity
-                 |intro;autobatch]
-              |rewrite > (swap_other a b a1)
-                 [rewrite > (not_eq_to_eqb_false a a1)
-                    [reflexivity
-                    |intro;autobatch]
-                 |assumption
-                 |intro;autobatch]]
-           |rewrite > H;rewrite > (swap_other a b x)
-              [elim (decidable_eq_nat a a1)
-                 [rewrite > H4;rewrite > swap_left;
-                  rewrite > (not_eq_to_eqb_false ? ? H3);reflexivity
-                 |elim (decidable_eq_nat b a1)
-                    [rewrite > H5;rewrite > swap_right;
-                     rewrite > (not_eq_to_eqb_false ? ? H2);reflexivity
-                    |rewrite > (swap_other a b a1)
-                       [rewrite > (not_eq_to_eqb_false ? ? H1);reflexivity
-                       |*:intro;autobatch]]]
-              |*:assumption]]]]]
-qed.
-
-lemma posn_swap : ∀a,b,x,vars.
-                  posn vars x = posn (swap_list a b vars) (swap a b x).
-intros 4;elim vars;simplify
-  [reflexivity
-  |rewrite < H;elim (decidable_eq_nat x a1)
-     [rewrite > H1;do 2 rewrite > eqb_n_n;reflexivity
-     |elim (decidable_eq_nat (swap a b x) (swap a b a1))
-        [elim H1;autobatch
-        |rewrite > (not_eq_to_eqb_false ? ? H1);
-         rewrite > (not_eq_to_eqb_false ? ? H2);reflexivity]]]
-qed.
-
 theorem encode_swap : ∀a,x,T,vars.
-                         ((in_list ? a (fv_NTyp T)) → (in_list ? a vars)) →
-                         (in_list ? x vars) →
+                         (a ∈ (fv_NTyp T) → a ∈ vars) →
+                         x ∈ vars →
                       encodetype T vars = 
                       encodetype (swap_NTyp a x T) (swap_list a x vars).
 intros 3;elim T
@@ -605,42 +369,13 @@ intros 3;elim T
 qed.
 
 lemma encode_swap2 : ∀a:nat.∀x:nat.∀T:NTyp.
-  ¬(in_list ? a (fv_NTyp T)) →
-    ∀vars.in_list ? x vars
-       →encodetype T vars=encodetype (swap_NTyp a x T) (swap_list a x vars).
+  a ∉ (fv_NTyp T) →
+    ∀vars.x ∈ vars
+       → encodetype T vars=encodetype (swap_NTyp a x T) (swap_list a x vars).
 intros;apply (encode_swap ? ? ? ? ? H1);intro;elim (H H2);
 qed.
 
-lemma remove_inlist : \forall x,y,l.(in_list ? x (remove_nat y l)) \to
-                      (in_list ? x l) \land x \neq y.
-intros 3;elim l 0;simplify;intro
-  [elim (not_in_list_nil ? ? H)
-  |elim (decidable_eq_nat y a)
-     [rewrite > H in H2;rewrite > eqb_n_n in H2;simplify in H2;
-      rewrite > H in H1;elim (H1 H2);rewrite > H;split
-        [apply in_list_cons;assumption
-        |assumption]
-     |rewrite > (not_eq_to_eqb_false ? ? H) in H2;simplify in H2;
-      inversion H2;intros;destruct;
-        [split;autobatch
-        |elim (H1 H3);split;autobatch]]]
-qed.
-
-lemma inlist_remove : ∀x,y,l.(in_list ? x l → x \neq y → 
-                (in_list ? x (remove_nat y l))).
-intros 3;elim l
-  [elim (not_in_list_nil ? ? H);
-  |simplify;elim (decidable_eq_nat y a)
-     [rewrite > (eq_to_eqb_true ? ? H3);simplify;apply H
-        [inversion H1;intros;destruct;
-           [elim H2;reflexivity
-           |assumption]
-        |assumption]
-     |rewrite > (not_eq_to_eqb_false ? ? H3);simplify;
-      inversion H1;intros;destruct;autobatch]]
-qed.
-
-lemma incl_fv_var : \forall T.(incl ? (fv_NTyp T) (var_NTyp T)).
+lemma incl_fv_var : \forall T.(fv_NTyp T) ⊆ (var_NTyp T).
 intro;elim T;simplify;unfold;intros
   [1,2:assumption
   |elim (in_list_append_to_or_in_list ? ? ? ? H2);autobatch
@@ -653,7 +388,7 @@ intro;elim T;simplify;unfold;intros
 qed.
 
 lemma fv_encode2 : ∀T,l1,l2.
-                      (∀x.(in_list ? x (fv_NTyp T)) →
+                      (∀x.x ∈ (fv_NTyp T) →
                            (lookup x l1 = lookup x l2 ∧
                             posn l1 x = posn l2 x)) →
                       (encodetype T l1 = encodetype T l2).
@@ -661,33 +396,10 @@ intros;apply fv_encode;intros;elim (H ? H1);split
   [assumption|intro;assumption]
 qed.
 
-lemma alpha_sym : \forall S,T.(alpha_eq S T) \to (alpha_eq T S).
-intros;elim H
-  [apply A_refl
-  |apply A_arrow;assumption
-  |apply A_forall
-     [assumption
-     |intros;apply H4;intro;apply H5;elim (decidable_eq_nat Z n5)
-        [rewrite > H7;apply in_list_head
-        |apply in_list_cons;inversion H6;intros;destruct;
-           [apply in_list_head
-           |apply in_list_cons;inversion H8;intros;destruct;
-              [elim H7;reflexivity
-              |elim (in_list_append_to_or_in_list ? ? ? ? H10);autobatch]]]]]
-qed.
-
-(*legacy*)
-lemma nat_in_list_case :∀G,H,n.in_list nat n (H@G) → 
-                         in_list nat n G ∨ in_list nat n H.
-intros;elim (in_list_append_to_or_in_list ???? H1)
-[right;assumption
-|left;assumption]
-qed.
-
 lemma inlist_fv_swap : ∀x,y,b,T.
-                   (¬ in_list ? b (y::var_NTyp T)) →
-                   in_list ? x (fv_NTyp (swap_NTyp b y T)) →
-                   x ≠ y ∧ (x = b ∨ (in_list ? x (fv_NTyp T))).
+                   b ∉ (y::var_NTyp T) →
+                   x ∈ (fv_NTyp (swap_NTyp b y T)) →
+                   x ≠ y ∧ (x = b ∨ x ∈ (fv_NTyp T)).
 intros 4;elim T
 [simplify in H;simplify;simplify in H1;elim (decidable_eq_nat y n)
  [rewrite > H2 in H1;rewrite > swap_right in H1;inversion H1;intros;destruct;
@@ -722,12 +434,9 @@ intros 4;elim T
    |elim H6
     [left;assumption
     |right;apply in_list_to_in_list_append_r;assumption]]
-  |intro;apply H2;elim (nat_in_list_case (var_NTyp n1) [y] ? H5)
-   [apply (in_list_to_in_list_append_r ? ? (y::var_NTyp n) (var_NTyp n1));
-    assumption
-   |inversion H6;intros;destruct;
-    [apply in_list_head
-    |elim (not_in_list_nil ? ? H7)]]
+  |intro;apply H2;elim (in_list_append_to_or_in_list ?? [y] (var_NTyp n1) H5)
+   [lapply (in_list_singleton_to_eq ??? H6);applyS in_list_head
+   |autobatch]
   |assumption]]
 |simplify;simplify in H3;simplify in H2;elim (in_list_append_to_or_in_list ? ? ? ? H3)
  [elim H
@@ -761,10 +470,10 @@ intros 4;elim T
 qed.
 
 lemma inlist_fv_swap_r : ∀x,y,b,T.
-                   (¬(in_list ? b (y::var_NTyp T))) →
-                   ((x = b ∧ (in_list ? y (fv_NTyp T))) ∨
-                    (x \neq y ∧ (in_list ? x (fv_NTyp T)))) →
-                   (in_list ? x (fv_NTyp (swap_NTyp b y T))).
+                   (b ∉ (y::var_NTyp T)) →
+                   ((x = b ∧ y ∈ (fv_NTyp T)) ∨
+                    (x ≠ y ∧ x ∈ (fv_NTyp T))) →
+                   x ∈ (fv_NTyp (swap_NTyp b y T)).
 intros 4;elim T
 [simplify;simplify in H;simplify in H1;cut (b ≠ n)
  [elim H1
@@ -842,90 +551,6 @@ intros 4;elim T
    |change in ⊢ (???%) with ((y::n::var_NTyp n1)@var_NTyp n2);autobatch]]
  |intro;apply H2;inversion H4;simplify;intros;destruct;autobatch depth=4]]
 qed.               
-
-lemma fv_alpha : ∀S,T.alpha_eq S T → incl ? (fv_NTyp S) (fv_NTyp T).
-intros;elim H;simplify;unfold;intros
-  [assumption
-  |elim (in_list_append_to_or_in_list ? ? ? ? H5);autobatch
-  |elim (in_list_append_to_or_in_list ? ? ? ? H5)
-     [autobatch
-     |elim (fresh_name (n4::n5::var_NTyp n1@var_NTyp n3));
-      apply in_list_to_in_list_append_r; 
-      lapply (H4 ? H7);
-      elim (remove_inlist ? ? ? H6);apply inlist_remove
-        [lapply (inlist_fv_swap_r x n4 a n1) 
-           [elim (inlist_fv_swap x n5 a n3)
-              [elim H11
-                 [rewrite < H12 in H7;elim H7;autobatch depth=5;
-                 |assumption]
-              |intro;apply H7;inversion H10;intros;destruct;autobatch depth=4
-              |autobatch]
-           |intro;apply H7;inversion H10;intros;destruct;autobatch depth=4
-           |right;split;assumption]
-        |intros;intro;lapply (inlist_fv_swap_r x n4 a n1)
-           [lapply (Hletin ? Hletin1);elim (inlist_fv_swap x n5 a n3 ? Hletin2)
-              [apply (H11 H10)
-              |intro;apply H7;elim (decidable_eq_nat a n4)
-                 [rewrite > H12;apply in_list_head
-                 |apply in_list_cons;inversion H11;intros;destruct;autobatch]]
-           |intro;apply H7;inversion H11;intros;destruct;autobatch depth=4
-           |right;split;assumption]]]]
-qed.
-
-theorem alpha_to_encode : ∀S,T.alpha_eq S T → 
-                             ∀vars.encodetype S vars = encodetype T vars.
-intros 3;elim H
-[reflexivity
-|simplify;rewrite > H2;rewrite > H4;reflexivity
-|simplify;rewrite > H2;
- cut (encodetype n1 (n4::vars) = encodetype n3 (n5::vars))
- [rewrite > Hcut;reflexivity
- |elim (fresh_name (n4::n5::var_NTyp n1@var_NTyp n3));
-  lapply (encode_swap2 a n4 n1 ? (n4::vars))
-  [intro;apply H5;autobatch depth=5
-  |lapply (encode_swap2 a n5 n3 ? (n5::vars))
-   [intro;autobatch depth=5
-   |rewrite > Hletin;rewrite > Hletin1;simplify;rewrite > swap_right;
-    rewrite > swap_right;rewrite > (H4 a H5 (a::swap_list a n4 vars));
-    rewrite > (fv_encode2 ? ? (a::swap_list a n5 vars))
-    [reflexivity
-    |intros;elim (decidable_eq_nat n4 n5)
-     [autobatch
-     |cut ((x ≠ n4) ∧ (x ≠ n5))
-      [elim Hcut;elim (decidable_eq_nat x a);simplify
-       [rewrite > (eq_to_eqb_true ? ? H10);simplify;autobatch
-       |rewrite > (not_eq_to_eqb_false ? ? H10);simplify;elim vars;simplify
-        [autobatch
-        |elim H11;rewrite < H12;rewrite > H13;elim (decidable_eq_nat a a1)
-         [rewrite > H14;do 2 rewrite > swap_left;
-          rewrite > (not_eq_to_eqb_false ? ? H8);  
-          rewrite > (not_eq_to_eqb_false ? ? H9);simplify;autobatch
-         |elim (decidable_eq_nat n4 a1)
-          [rewrite > H15;rewrite > swap_right;rewrite > (swap_other a n5 a1)
-           [rewrite > (not_eq_to_eqb_false ? ? H10);rewrite < H15;
-            rewrite > (not_eq_to_eqb_false ? ? H8);autobatch
-           |intro;autobatch
-           |intro;autobatch]
-          |rewrite > (swap_other a n4 a1);elim (decidable_eq_nat n5 a1)
-           [rewrite < H16;rewrite > swap_right;
-            rewrite > (not_eq_to_eqb_false ? ? H9);
-            rewrite > (not_eq_to_eqb_false ? ? H10);autobatch
-           |rewrite > (swap_other a n5 a1);try intro;autobatch
-           |*:intro;autobatch]]]]]
-      |split
-       [lapply (H3 ? H5);lapply (alpha_sym ? ? Hletin2);
-        lapply (fv_alpha ? ? Hletin3);lapply (Hletin4 ? H6);
-        elim (inlist_fv_swap ? ? ? ? ? Hletin5)
-        [assumption
-        |intro;apply H5;inversion H8;intros;destruct;autobatch depth=4]
-       |elim (inlist_fv_swap ? ? ? ? ? H6)
-        [assumption
-        |intro;apply H5;elim (decidable_eq_nat a n4)
-         [applyS in_list_head
-         |apply in_list_cons;inversion H8;intros;destruct;autobatch]]]]]]
-   |apply in_list_head]
-  |apply in_list_head]]]
-qed.
                       
 lemma encode_append : ∀T,U,n,l.length ? l ≤ n →
         subst_type_nat (encodetype T l) U n = encodetype T l.
@@ -937,8 +562,8 @@ intros 2;elim T;simplify
         |intro;rewrite > H2 in Hletin1;unfold in Hletin1;autobatch]
      |cut (lookup n l = false)
         [rewrite > Hcut;reflexivity
-        |generalize in match H1;elim (lookup n l);
-           [elim H2;reflexivity|reflexivity]]]
+        |elim (lookup n l) in H1;
+           [elim H1;reflexivity|reflexivity]]]
   |reflexivity
   |autobatch
   |rewrite > (H ? ? H2);rewrite > H1;
@@ -950,30 +575,30 @@ lemma encode_subst_simple : ∀X,T,l.
   encodetype T l = subst_type_nat (encodetype T (l@[X])) (TFree X) (length ? l).
 intros 2;elim T;simplify
 [cut (lookup n l = true → posn l n = posn (l@[X]) n)
- [generalize in match Hcut;elim (bool_to_decidable_eq (lookup n l) true)
+ [elim (bool_to_decidable_eq (lookup n l) true) in Hcut
   [cut (lookup n (l@[X]) = true)
-   [rewrite > H;rewrite > Hcut1;simplify;
+   [rewrite > H;rewrite > Hcut;simplify;
     cut (eqb (posn (l@[X]) n) (length nat l) = false)
-    [rewrite > Hcut2;simplify;rewrite < (H1 H);reflexivity
-    |generalize in match H;elim l 0
-     [simplify;intro;destruct H2
+    [rewrite > Hcut1;simplify;rewrite < (H1 H);reflexivity
+    |elim l in H 0
+     [simplify;intro;destruct
      |intros 2;simplify;elim (eqb n a);simplify
       [reflexivity
-      |simplify in H3;apply (H2 H3)]]]
-   |generalize in match H;elim l
-    [simplify in H2;destruct H2
-    |generalize in match H3;simplify;elim (eqb n a) 0;simplify;intro
+      |simplify in H3;apply (H H2)]]]
+   |elim l in H
+    [simplify in H;destruct
+    |generalize in match H2;simplify;elim (eqb n a) 0;simplify;intro
      [reflexivity
-     |apply (H2 H4)]]]
+     |apply (H H3)]]]
   |cut (lookup n l = false)
    [elim (decidable_eq_nat n X)
-    [rewrite > Hcut1;rewrite > H2;cut (lookup X (l@[X]) = true)
-     [rewrite > Hcut2;simplify;cut (eqb (posn (l@[X]) X) (length nat l) = true)
-      [rewrite > Hcut3;simplify;reflexivity
-      |generalize in match Hcut1;elim l 0
+    [rewrite > Hcut;rewrite > H2;cut (lookup X (l@[X]) = true)
+     [rewrite > Hcut1;simplify;cut (eqb (posn (l@[X]) X) (length nat l) = true)
+      [rewrite > Hcut2;simplify;reflexivity
+      |elim l in Hcut 0
        [intros;simplify;rewrite > eqb_n_n;simplify;reflexivity
        |simplify;intros 2;rewrite > H2;elim (eqb X a);simplify in H4
-        [destruct H4
+        [destruct
         |apply (H3 H4)]]]
      |elim l;simplify
       [rewrite > eqb_n_n;reflexivity
@@ -981,16 +606,16 @@ intros 2;elim T;simplify
        [reflexivity
        |assumption]]]
     |cut (lookup n l = lookup n (l@[X]))
-     [rewrite < Hcut2;rewrite > Hcut1;simplify;reflexivity
+     [rewrite < Hcut1;rewrite > Hcut;simplify;reflexivity
      |elim l;simplify
       [rewrite > (not_eq_to_eqb_false ? ? H2);simplify;reflexivity
       |elim (eqb n a);simplify
        [reflexivity
        |assumption]]]]
-   |generalize in match H;elim (lookup n l);
-    [elim H2;reflexivity|reflexivity]]]
+   |elim (lookup n l) in H
+    [elim H;reflexivity|reflexivity]]]
  |elim l 0
-  [intro;simplify in H;destruct H
+  [intro;simplify in H;destruct
   |simplify;intros 2;elim (eqb n a);simplify
    [reflexivity
    |simplify in H1;rewrite < (H H1);reflexivity]]]
@@ -1000,8 +625,8 @@ intros 2;elim T;simplify
  rewrite < (H1 ([n]@l));reflexivity]
 qed.
 
-lemma encode_subst : ∀T,X,Y,l.¬(in_list ? X l) → ¬(in_list ? Y l) →
-                              (in_list ? X (fv_NTyp T) → X = Y) → 
+lemma encode_subst : ∀T,X,Y,l.X ∉ l → Y ∉ l →
+                              (X ∈ (fv_NTyp T) → X = Y) → 
                               encodetype (swap_NTyp X Y T) l =
                  subst_type_nat (encodetype T (l@[Y])) (TFree X) (length ? l).
 apply NTyp_len_ind;intro;elim U
@@ -1012,11 +637,11 @@ apply NTyp_len_ind;intro;elim U
    [simplify;rewrite > Hcut;rewrite > (not_nat_in_to_lookup_false ? ? H2);
     simplify;cut (posn (l@[Y]) Y = length ? l)
     [rewrite > Hcut1;rewrite > eqb_n_n;reflexivity
-    |generalize in match H2;elim l;simplify
+    |elim l in H2;simplify
      [rewrite > eqb_n_n;reflexivity
      |elim (decidable_eq_nat Y a)
-      [elim H6;rewrite > H7;apply in_list_head
-      |rewrite > (not_eq_to_eqb_false ? ? H7);simplify;rewrite < H5
+      [elim H5;rewrite > H6;apply in_list_head
+      |rewrite > (not_eq_to_eqb_false ? ? H6);simplify;rewrite < H2
        [reflexivity
        |intro;autobatch]]]]
    |elim l;simplify
@@ -1029,11 +654,11 @@ apply NTyp_len_ind;intro;elim U
    cut (lookup Y (l@[Y]) = true)
    [rewrite > Hcut;simplify;cut (posn (l@[Y]) Y = length ? l)
     [rewrite > Hcut1;rewrite > eqb_n_n;reflexivity
-    |generalize in match H2;elim l;simplify
+    |elim l in H2;simplify
      [rewrite > eqb_n_n;reflexivity
      |elim (decidable_eq_nat Y a)
-      [elim H7;rewrite > H8;apply in_list_head
-      |rewrite > (not_eq_to_eqb_false ? ? H8);simplify;rewrite < H6
+      [elim H6;applyS in_list_head
+      |rewrite > (not_eq_to_eqb_false ? ? H7);simplify;rewrite < H2
        [reflexivity
        |intro;autobatch]]]]
    |elim l;simplify
@@ -1042,17 +667,16 @@ apply NTyp_len_ind;intro;elim U
   |simplify;rewrite > (swap_other X Y n)
    [cut (lookup n l = lookup n (l@[Y]) ∧ 
          (lookup n l = true → posn l n = posn (l@[Y]) n))
-    [elim Hcut;rewrite > H6;generalize in match H7;
-     generalize in match H6;elim (lookup n (l@[Y]));simplify;
-     [rewrite < H9;generalize in match H8;elim l
-      [simplify in H10;destruct H10;
+    [elim Hcut;rewrite > H6;elim (lookup n (l@[Y])) in H7 H6;simplify;
+     [rewrite < H7;elim l in H6
+      [simplify in H6;destruct
       |elim (decidable_eq_nat n a);simplify
-       [rewrite > (eq_to_eqb_true ? ? H12);reflexivity
-       |rewrite > (not_eq_to_eqb_false ? ? H12);
-        simplify;generalize in match H10;elim (eqb (posn l1 n) (length nat l1))
-        [simplify in H13;simplify in H11;
-         rewrite > (not_eq_to_eqb_false ? ? H12) in H11;
-         simplify in H11;lapply (H13 H11);destruct Hletin
+       [rewrite > (eq_to_eqb_true ? ? H9);reflexivity
+       |rewrite > (not_eq_to_eqb_false ? ? H9);
+        simplify;elim (eqb (posn l1 n) (length nat l1)) in H6
+        [simplify in H8;simplify in H6;
+         rewrite > (not_eq_to_eqb_false ? ? H9) in H8;
+         simplify in H8;lapply (H6 H8);destruct
         |reflexivity]]
       |*:assumption]
      |reflexivity]
@@ -1076,14 +700,14 @@ apply NTyp_len_ind;intro;elim U
  |intro;apply H5;simplify;autobatch]
 |simplify;rewrite < (H2 n1 ? ? ? ? H3 H4) 
  [cut (l = swap_list X Y l)
-  [|generalize in match H3;generalize in match H4;elim l;simplify
+  [|elim l in H3 H4;simplify
    [reflexivity
    |elim (decidable_eq_nat a X)
-    [elim H8;rewrite > H9;apply in_list_head
+    [elim H4;applyS in_list_head
     |elim (decidable_eq_nat a Y)
-     [elim H7;rewrite > H10;apply in_list_head
+     [elim H6;applyS in_list_head
      |rewrite > (swap_other X Y a)
-      [rewrite < H6
+      [rewrite < H3
        [reflexivity
        |*:intro;autobatch]
       |*:assumption]]]]]
@@ -1153,13 +777,7 @@ apply NTyp_len_ind;intro;elim U
  |intro;apply H5;simplify;autobatch]]
 qed.
 
-lemma swap_case: ∀u,v,x.(swap u v x) = u ∨ (swap u v x) = v ∨ (swap u v x = x).
-intros;unfold in match swap;simplify;elim (eqb x u);simplify
-  [autobatch
-  |elim (eqb x v);simplify;autobatch]
-qed.
-
-lemma in_fvNTyp_in_fvNenv : ∀G,T.(NWFType G T) → (incl ? (fv_NTyp T) (fv_Nenv G)).
+lemma in_fvNTyp_in_fvNenv : ∀G,T.(NWFType G T) → (fv_NTyp T) ⊆ (fv_Nenv G).
 intros;elim H;simplify;unfold;intros;
 [inversion H2;intros;destruct;
  [assumption
@@ -1202,8 +820,14 @@ intros;elim H;simplify;unfold;intros;
         autobatch depth=5
        |apply (in_remove ? ? ? H15 H16)]]
      |simplify;simplify in H13;elim (remove_inlist ? ? ? H13);
-      elim (nat_in_list_case ? ? ? H14);
-      [apply in_list_to_in_list_append_r;apply in_remove;
+      elim (in_list_append_to_or_in_list ???? H14)
+      [apply in_list_to_in_list_append_l;apply H10;
+       [rewrite < (associative_append ? [x] (fv_Nenv l) (var_NTyp n4));
+        intro;apply H12;simplify;
+        rewrite < (associative_append ? [x] (fv_Nenv l) (n3::var_NTyp n4@var_NTyp n5));
+        elim (in_list_append_to_or_in_list ???? H17);autobatch depth=4
+       |autobatch]
+      |apply in_list_to_in_list_append_r;apply in_remove;
        [elim (remove_inlist ? ? ? H16);intro;apply H18;
         elim (swap_case a n n3)
         [elim H20
@@ -1214,14 +838,8 @@ intros;elim H;simplify;unfold;intros;
         [rewrite < (associative_append ? [x] (fv_Nenv l) (var_NTyp n5));
          intro;apply H12;simplify;
          rewrite < (associative_append ? [x] (fv_Nenv l) (n3::var_NTyp n4 @ var_NTyp n5));
-         elim (nat_in_list_case ? ? ? H17);autobatch depth=4
-        |elim (remove_inlist ? ? ? H16);autobatch]]
-      |apply in_list_to_in_list_append_l;apply H10;
-       [rewrite < (associative_append ? [x] (fv_Nenv l) (var_NTyp n4));
-        intro;apply H12;simplify;
-        rewrite < (associative_append ? [x] (fv_Nenv l) (n3::var_NTyp n4@var_NTyp n5));
-        elim (nat_in_list_case ? ? ? H17);autobatch depth=4
-       |autobatch]]]]
+         elim (in_list_append_to_or_in_list ???? H17);autobatch depth=4
+        |elim (remove_inlist ? ? ? H16);autobatch]]]]]
    |split
     [intro;apply H7;rewrite > H8;apply in_list_head
     |elim (remove_inlist ? ? ? H6);assumption]]
@@ -1229,8 +847,8 @@ intros;elim H;simplify;unfold;intros;
   |right;intro;autobatch depth=5]]]
 qed.
 
-lemma fv_NTyp_fv_Typ : ∀T,X,l.(in_list ? X (fv_NTyp T)) → ¬(in_list ? X l) → 
-                          (in_list ? X (fv_type (encodetype T l))).
+lemma fv_NTyp_fv_Typ : ∀T,X,l.X ∈ (fv_NTyp T) → X ∉ l → 
+                          X ∈ (fv_type (encodetype T l)).
 intros 2;elim T;simplify
   [simplify in H;cut (X = n)
      [rewrite < Hcut;generalize in match (lookup_in X l);elim (lookup X l)
@@ -1291,8 +909,8 @@ intros;elim H;simplify
   |*:apply not_in_list_nil]]] 
 qed.
 
-lemma not_in_list_encodetype : \forall T,l,x.in_list ? x l \to
-                      \lnot (in_list ? x (fv_type (encodetype T l))).
+lemma not_in_list_encodetype : \forall T,l,x.x ∈ l \to
+                      \lnot x ∈ (fv_type (encodetype T l)).
 intro;elim T;simplify
   [apply (bool_elim ? (lookup n l));intro;simplify
      [apply not_in_list_nil
@@ -1300,13 +918,13 @@ intro;elim T;simplify
         [rewrite > (in_lookup ? ? H) in H1;destruct H1
         |apply (not_in_list_nil ? ? H3)]]
   |apply not_in_list_nil
-  |intro;elim (nat_in_list_case ? ? ? H3);autobatch
-  |intro;elim (nat_in_list_case ? ? ? H3);
-     [apply (H1 (n::l) x ? H4);apply in_list_cons;assumption
-     |autobatch]]
+  |intro;elim (in_list_append_to_or_in_list ???? H3);autobatch
+  |intro;elim (in_list_append_to_or_in_list ???? H3);
+     [autobatch
+     |apply (H1 (n::l) x ? H4);apply in_list_cons;assumption]]
 qed.
 
-lemma incl_fv_encode_fv : \forall T,l.incl ? (fv_type (encodetype T l)) (fv_NTyp T).
+lemma incl_fv_encode_fv : \forall T,l.(fv_type (encodetype T l)) ⊆ (fv_NTyp T).
 intro;elim T;simplify;unfold;
   [intro;elim (lookup n l);simplify in H
      [elim (not_in_list_nil ? ? H)
@@ -1374,7 +992,7 @@ lemma adeq_WFE : ∀G.NWFEnv G → WFEnv (encodeenv G).
 intros;elim H;simplify;autobatch;
 qed.
 
-lemma NWFT_env_incl : ∀G,T.NWFType G T → ∀H.incl ? (fv_Nenv G) (fv_Nenv H) 
+lemma NWFT_env_incl : ∀G,T.NWFType G T → ∀H.(fv_Nenv G) ⊆ (fv_Nenv H) 
                       → NWFType H T.
 intros 3;elim H
   [4:apply NWFT_Forall
@@ -1382,7 +1000,9 @@ intros 3;elim H
      |intros;apply (H4 ? ? H8);
         [intro;apply H7;apply (H6 ? H9)
         |unfold;intros;simplify;simplify in H9;inversion H9;intros;
-         destruct;autobatch]]
+         destruct;simplify;
+         [autobatch
+         |apply in_list_cons;apply H6;apply H10]]]
   |*:autobatch]
 qed.
 
@@ -1394,13 +1014,11 @@ intros;elim H
         [elim (not_in_list_nil ? ? H1)
         |inversion H6;intros;destruct;
            [simplify;autobatch
-           |elim a;simplify;autobatch]]
+           |elim a;simplify;elim b;simplify;try apply in_list_cons;
+            apply H1;apply H7]]
      |assumption]
   |elim H2;elim H4;split;autobatch
-  |split;assumption
-  |elim H2;split
-     [lapply (adeq_WFT ? ? H5);autobatch;
-     |lapply (adeq_WFT ? ? H6);autobatch]]
+  |split;assumption]
 qed.
 
 theorem adequacy : ∀G,T,U.NJSubtype G T U → 
@@ -1420,25 +1038,21 @@ intros;elim H;simplify
             apply (H6 ? H7)
               [elim (decidable_eq_nat X n)
                  [left;assumption
-                 |right;intro;lapply (in_remove ? ? ? H10 H11);elim H7;
-                  autobatch]
+                 |right;intro;autobatch depth=5]
               |elim (decidable_eq_nat X n1)
                  [left;assumption
-                 |right;intro;lapply (in_remove ? ? ? H10 H11);elim H7;
-                  autobatch]]
-           |2,3:apply not_in_list_nil
+                 |right;intro;autobatch depth=5]]
+           |2,3:autobatch
            |intro;elim (NJSubtype_to_NWFT ? ? ? Hletin);
             lapply (in_fvNTyp_in_fvNenv ? ? H10);simplify in Hletin1;
             elim (decidable_eq_nat X n1)
               [assumption
-              |lapply (in_remove ? ? ? H11 H8);elim H7;autobatch]]
+              |elim H7;autobatch depth=4]]
         |2,3:autobatch
         |intro;elim (NJSubtype_to_NWFT ? ? ? Hletin);lapply (in_fvNTyp_in_fvNenv ? ? H9);
          simplify in Hletin1;elim (decidable_eq_nat X n)
            [assumption
-           |lapply (in_remove ? ? ? H11 H8);elim H7;autobatch]]]
-  |rewrite < (alpha_to_encode ? ? H3);rewrite < (alpha_to_encode ? ? H4);
-   assumption]
+           |elim H7;autobatch depth=4]]]]
 qed.
 
 let rec closed_type T n ≝
@@ -1449,58 +1063,9 @@ let rec closed_type T n ≝
     | Arrow T1 T2 ⇒ closed_type T1 n ∧ closed_type T2 n
     | Forall T1 T2 ⇒  closed_type T1 n ∧ closed_type T2 (S n)].
     
-alias id "nth" = "cic:/matita/list/list/nth.con".
-alias id "length" = "cic:/matita/list/list/length.con".
-definition distinct_list ≝
-λl.∀n,m.n < length ? l → m < length ? l → n ≠ m → nth ? l O n ≠ nth ? l O m.
-
-lemma posn_nth: ∀l,n.distinct_list l → n < length ? l → 
-                    posn l (nth ? l O n) = n.
-intro;elim l
-  [simplify in H1;elim (not_le_Sn_O ? H1)
-  |simplify in H2;generalize in match H2;elim n
-     [simplify;rewrite > eqb_n_n;simplify;reflexivity
-     |simplify;cut (nth ? (a::l1) O (S n1) ≠ nth ? (a::l1) O O)
-        [simplify in Hcut;rewrite > (not_eq_to_eqb_false ? ? Hcut);simplify;
-         rewrite > (H n1)
-           [reflexivity
-           |unfold;intros;unfold in H1;lapply (H1 (S n2) (S m));
-              [simplify in Hletin;assumption
-              |2,3:simplify;autobatch
-              |intro;apply H7;destruct H8;reflexivity]
-           |autobatch]
-        |intro;apply H1;
-           [6:apply H5
-           |skip
-           |skip
-           |(*** *:autobatch; *)
-            apply H4
-           |simplify;autobatch
-           |intro;elim (not_eq_O_S n1);symmetry;assumption]]]]
-qed.
-
-lemma nth_in_list : ∀l,n. n < length ? l → in_list ? (nth ? l O n) l.
-intro;elim l
-  [simplify in H;elim (not_le_Sn_O ? H)
-  |generalize in match H1;elim n;simplify
-     [apply in_list_head
-     |apply in_list_cons;apply H;simplify in H3;apply (le_S_S_to_le ? ? H3)]]
-qed.
-
-lemma lookup_nth : \forall l,n.n < length ? l \to 
-                   lookup (nth nat l O n) l = true.
-intro;elim l
-  [elim (not_le_Sn_O ? H);
-  |generalize in match H1;elim n;simplify
-     [rewrite > eqb_n_n;reflexivity
-     |elim (eqb (nth nat l1 O n1) a);simplify;
-        [reflexivity
-        |apply H;apply le_S_S_to_le;assumption]]]
-qed.
-    
 lemma decoder : ∀T,n.closed_type T n → 
                      ∀l.length ? l = n → distinct_list l →
-                  (\forall x. in_list ? x (fv_type T) \to \lnot in_list ? x l) \to   
+                  (\forall x. x ∈ (fv_type T) \to x ∉ l) \to   
                      ∃U.T = encodetype U l.
 intro;elim T
   [simplify in H;apply (ex_intro ? ? (TName (nth ? l O n)));simplify;
@@ -1581,10 +1146,10 @@ intros 2;elim H 0
      |elim a in H6;simplify in H6;destruct H6;apply NWFE_cons;autobatch]]
 qed.
 
-lemma xxx : \forall b,X,T,l.
+lemma in_list_encodeenv : \forall b,X,T,l.
             in_list ? (mk_bound b X (encodetype T [])) (encodeenv l) \to
             \exists U.encodetype U [] = encodetype T [] \land
-                      in_list ? (mk_nbound b X U) l.
+                      (mk_nbound b X U) ∈ l.
 intros 4;elim l
   [simplify in H;elim (not_in_list_nil ? ? H)
   |simplify in H1;inversion H1;elim a 0;simplify;intros;destruct;
@@ -1593,9 +1158,9 @@ intros 4;elim l
 qed.
 
 lemma eq_swap_NTyp_to_case :
-  \forall X,Y,Z,T.\lnot in_list ? Y (X::var_NTyp T) \to
+  \forall X,Y,Z,T. Y ∉ (X::var_NTyp T) \to
     swap_NTyp Z Y (swap_NTyp Y X T) = swap_NTyp Z X T \to
-      Z = X \lor \lnot in_list ? Z (fv_NTyp T).
+      Z = X \lor Z ∉ (fv_NTyp T).
 intros 4;elim T
   [simplify in H;simplify in H1;elim (decidable_eq_nat X n)
      [rewrite > H2;simplify;elim (decidable_eq_nat Z n)
@@ -1661,10 +1226,9 @@ intros 4;elim H 0
      |rewrite > H3 in H2;rewrite < eq_fv_Nenv_fv_env in H2;assumption]
   |intros;cut (T2 = TName n) 
      [|elim T2 in H5 0;simplify;intros;destruct;reflexivity]
-   rewrite > Hcut;
-   elim (decoder t1 O ? []);
-     [rewrite > H4 in H1;rewrite > H7 in H1;elim (xxx ? ? ? ? H1);elim H8;
-      autobatch
+   rewrite > Hcut;elim (decoder t1 O ? []);
+     [rewrite > H4 in H1;rewrite > H7 in H1;elim (in_list_encodeenv ???? H1);
+      elim H8;autobatch
      |4:unfold;intros;simplify in H7;elim (not_le_Sn_O ? H7)
      |*:autobatch]
   |intros;cut (∃u,u1,u2,u3.T2 = NArrow u u1 ∧ U2 = NArrow u2 u3)
diff --git a/helm/software/matita/contribs/POPLmark/Fsub/defn.ma b/helm/software/matita/contribs/POPLmark/Fsub/defn.ma
index cd7bbfdfe..337fe2686 100644
--- a/helm/software/matita/contribs/POPLmark/Fsub/defn.ma
+++ b/helm/software/matita/contribs/POPLmark/Fsub/defn.ma
@@ -45,8 +45,11 @@ let rec subst_type_nat T U i ≝
 
 (*** definitions about lists ***)
 
+definition filter_types : list bound → list bound ≝
+  λG.(filter ? G (λB.match B with [mk_bound B X T ⇒ B])).
+
 definition fv_env : list bound → list nat ≝
-  λG.(map ? ? (λb.match b with [mk_bound B X T ⇒ X]) G).
+  λG.(map ? ? (λb.match b with [mk_bound B X T ⇒ X]) (filter_types G)).
 
 let rec fv_type T ≝
   match T with
@@ -92,13 +95,21 @@ inductive JSubtype : list bound → Typ → Typ → Prop ≝
                 (subst_type_nat S2 (TFree X) O) (subst_type_nat T2 (TFree X) O)) →
              JSubtype G (Forall S1 S2) (Forall T1 T2).
 
-notation "hvbox(e ⊢ break ta ⊴  break tb)" 
+notation "mstyle color #007f00 (hvbox(e ⊢ break ta ⊴ break tb))" 
   non associative with precedence 30 for @{ 'subjudg $e $ta $tb }.  
 interpretation "Fsub subtype judgement" 'subjudg e ta tb = (JSubtype e ta tb).
 
-notation > "hvbox(\Forall S.T)" 
+notation "mstyle color #007f00 (hvbox(e ⊢ ♦))" 
+  non associative with precedence 30 for @{ 'wfejudg $e }.  
+interpretation "Fsub WF env judgement" 'wfejudg e = (WFEnv e).
+
+notation "mstyle color #007f00 (hvbox(e ⊢ break t))" 
+  non associative with precedence 30 for @{ 'wftjudg $e $t }.  
+interpretation "Fsub WF type judgement" 'wftjudg e t = (WFType e t).
+
+notation > "\Forall S.T" 
   non associative with precedence 60 for @{ 'forall $S $T}.
-notation < "hvbox('All' \sub S. break T)" 
+notation < "hvbox(⊓ \sub S. break T)" 
   non associative with precedence 60 for @{ 'forall $S $T}.
 interpretation "universal type" 'forall S T = (Forall S T).
   
@@ -115,7 +126,7 @@ notation "hvbox(s break ⇛ t)"
   right associative with precedence 55 for @{ 'arrow $s $t }.
 interpretation "arrow type" 'arrow S T = (Arrow S T).
   
-notation "hvbox(S [# n ↦ T])"
+notation "hvbox(S [#n ↦ T])"
   non associative with precedence 80 for @{ 'substvar $S $T $n }.
 interpretation "subst bound var" 'substvar S T n = (subst_type_nat S T n).  
 
@@ -127,37 +138,32 @@ interpretation "subtyping bound" 'subtypebound X T = (mk_bound true X T).
 
 (*** theorems about lists ***)
 
-lemma boundinenv_natinfv : ∀x,G.(∃B,T.in_list ? (mk_bound B x T) G) →
-                              in_list ? x (fv_env G).
+lemma boundinenv_natinfv : ∀x,G.(∃T.!x ⊴ T ∈ G) → x ∈ (fv_env G).
 intros 2;elim G;decompose
-  [elim (not_in_list_nil ? ? H)
-  |elim (in_list_cons_case ? ? ? ? H1)
-     [rewrite < H2;simplify;apply in_list_head
-     |simplify;apply in_list_cons;apply H;autobatch]]
+  [elim (not_in_list_nil ? ? H1)
+  |elim (in_list_cons_case ? ? ? ? H2)
+     [rewrite < H1;simplify;apply in_list_head
+     |elim a;apply (bool_elim ? b);intro;simplify;try apply in_list_cons;
+      apply H;autobatch]]
 qed.
 
-lemma natinfv_boundinenv : ∀x,G.in_list ? x (fv_env G) →
-                              ∃B,T.in_list ? (mk_bound B x T) G.
+lemma natinfv_boundinenv : ∀x,G.x ∈ (fv_env G) → ∃T.!x ⊴ T ∈ G.
 intros 2;elim G 0
   [simplify;intro;lapply (not_in_list_nil ? ? H);elim Hletin
   |intros 3;
-   elim a;simplify in H1;elim (in_list_cons_case ? ? ? ? H1)
+   elim a;simplify in H1;elim b in H1;simplify in H1
+   [elim (in_list_cons_case ? ? ? ? H1)
      [rewrite < H2;autobatch
-     |elim (H H2);elim H3;apply ex_intro[apply a1];autobatch]]
+     |elim (H H2);autobatch]
+   |elim (H H1);autobatch]]
 qed.
 
-lemma incl_bound_fv : ∀l1,l2.incl ? l1 l2 → incl ? (fv_env l1) (fv_env l2).
+lemma incl_bound_fv : ∀l1,l2.l1 ⊆ l2 → (fv_env l1) ⊆ (fv_env l2).
 intros;unfold in H;unfold;intros;apply boundinenv_natinfv;
 lapply (natinfv_boundinenv ? ? H1);decompose;autobatch depth=4;
 qed.
 
-lemma incl_cons : ∀x,l1,l2.incl ? l1 l2 → incl nat (x :: l1) (x :: l2).
-intros.unfold in H.unfold.intros.elim (in_list_cons_case ? ? ? ? H1)
-  [applyS in_list_head|autobatch]
-qed.
-
-lemma WFT_env_incl : ∀G,T.WFType G T → 
-                       ∀H.incl ? (fv_env G) (fv_env H) → WFType H T.
+lemma WFT_env_incl : ∀G,T.(G ⊢ T) → ∀H.fv_env G ⊆ fv_env H → (H ⊢ T).
 intros 3.elim H
   [apply WFT_TFree;unfold in H3;apply (H3 ? H1)
   |apply WFT_Top
@@ -166,19 +172,21 @@ intros 3.elim H
      [apply (H2 ? H6)
      |intros;apply (H4 ? ? H8)
         [unfold;intro;autobatch
-        |simplify;apply (incl_cons ? ? ? H6)]]]
+        |simplify;apply (incl_cons ???? H6)]]]
 qed.
 
-lemma fv_env_extends : ∀H,x,B,C,T,U,G.
-                          fv_env (H @ ((mk_bound B x T) :: G)) = 
-                          fv_env (H @ ((mk_bound C x U) :: G)).
-intros;elim H
-  [reflexivity|elim a;simplify;rewrite > H1;reflexivity]
+lemma fv_env_extends : ∀H,x,T,U,G,B.
+                         fv_env (H @ mk_bound B x T :: G) = 
+                         fv_env (H @ mk_bound B x U :: G).
+intros 5;elim H;elim B
+  [1,2:reflexivity
+  |*:elim a;elim b;simplify;lapply (H1 true);lapply (H1 false);
+   try rewrite > Hletin;try rewrite > Hletin1;reflexivity]
 qed.
 
 lemma lookup_env_extends : ∀G,H,B,C,D,T,U,V,x,y.
-            in_list ? (mk_bound D y V) (H @ ((mk_bound C x U) :: G)) → y ≠ x → 
-            in_list ? (mk_bound D y V) (H @ ((mk_bound B x T) :: G)).
+            mk_bound D y V ∈ H @ mk_bound C x U :: G → y ≠ x → 
+            mk_bound D y V ∈ H @ mk_bound B x T :: G.
 intros 10;elim H
   [simplify in H1;elim (in_list_cons_case ? ? ? ? H1)
      [destruct H3;elim H2;reflexivity
@@ -188,8 +196,7 @@ intros 10;elim H
      |apply (in_list_cons ? ? ? ? (H1 H4 H3))]]
 qed.
 
-lemma in_FV_subst : ∀x,T,U,n.in_list ? x (fv_type T) →
-                                in_list ? x (fv_type (subst_type_nat T U n)).
+lemma in_FV_subst : ∀x,T,U,n.x ∈ fv_type T → x ∈ fv_type (subst_type_nat T U n).
 intros 3;elim T
   [simplify in H;elim (not_in_list_nil ? ? H)
   |2,3:simplify;simplify in H;assumption
@@ -199,7 +206,7 @@ qed.
 
 (*** lemma on fresh names ***)
 
-lemma fresh_name : ∀l:list nat.∃n.¬in_list ? n l.
+lemma fresh_name : ∀l:list nat.∃n.n ∉ l.
 cut (∀l:list nat.∃n.∀m.n ≤ m → ¬ in_list ? m l);intros
   [lapply (Hcut l);elim Hletin;apply ex_intro;autobatch
   |elim l
@@ -215,8 +222,7 @@ qed.
 
 (*** lemmata on well-formedness ***)
 
-lemma fv_WFT : ∀T,x,G.WFType G T → in_list ? x (fv_type T) →
-                    in_list ? x (fv_env G).
+lemma fv_WFT : ∀T,x,G.(G ⊢ T) → x ∈ fv_type T → x ∈ fv_env G.
 intros 4.elim H
   [simplify in H2;elim (in_list_cons_case ? ? ? ? H2)
      [applyS H1|elim (not_in_list_nil ? ? H3)]
@@ -238,11 +244,11 @@ qed.
 
 (*** lemmata relating subtyping and well-formedness ***)
 
-lemma JS_to_WFE : ∀G,T,U.G ⊢ T ⊴ U → WFEnv G.
+lemma JS_to_WFE : ∀G,T,U.G ⊢ T ⊴ U → G ⊢ ♦.
 intros;elim H;assumption.
 qed.
 
-lemma JS_to_WFT : ∀G,T,U.G ⊢ T ⊴ U → WFType G T ∧ WFType G U.
+lemma JS_to_WFT : ∀G,T,U.G ⊢ T ⊴ U → (G ⊢ T) ∧ (G ⊢ U).
 intros;elim H
   [1,2:autobatch
   |split 
@@ -256,18 +262,18 @@ intros;elim H
       apply (WFT_env_incl ? ? H10);simplify;unfold;intros;assumption]]
 qed.
 
-lemma JS_to_WFT1 : ∀G,T,U.G ⊢ T ⊴ U → WFType G T.
+lemma JS_to_WFT1 : ∀G,T,U.G ⊢ T ⊴ U → G ⊢ T.
 intros;elim (JS_to_WFT ? ? ? H);assumption;
 qed.
 
-lemma JS_to_WFT2 : ∀G,T,U.G ⊢ T ⊴ U → WFType G U.
+lemma JS_to_WFT2 : ∀G,T,U.G ⊢ T ⊴ U → G ⊢ U.
 intros;elim (JS_to_WFT ? ? ? H);assumption;
 qed.
 
-lemma WFE_Typ_subst : ∀H,x,B,C,T,U,G.
-                      WFEnv (H @ ((mk_bound B x T) :: G)) → WFType G U →
-                      WFEnv (H @ ((mk_bound C x U) :: G)).
-intros 7;elim H 0
+lemma WFE_Typ_subst : ∀H,x,B,T,U,G.
+                      H @ mk_bound B x T :: G ⊢ ♦ → (G ⊢ U) →
+                      H @ mk_bound B x U :: G ⊢ ♦.
+intros 6;elim H 0
   [simplify;intros;inversion H1;intros
      [elim (nil_cons ? G (mk_bound B x T) H3)
      |destruct H7;autobatch]
@@ -276,15 +282,14 @@ intros 7;elim H 0
      [destruct H5
      |destruct H9;apply WFE_cons
         [apply (H1 H5 H3)
-        |rewrite < (fv_env_extends ? x B C T U); assumption
+        |rewrite < (fv_env_extends ? x T U); assumption
         |apply (WFT_env_incl ? ? H8);
-         rewrite < (fv_env_extends ? x B C T U);unfold;intros;
+         rewrite < (fv_env_extends ? x T U);unfold;intros;
          assumption]]]
 qed.
 
-lemma WFE_bound_bound : ∀B,x,T,U,G.WFEnv G → in_list ? (mk_bound B x T) G →
-                        in_list ? (mk_bound B x U) G → T = U.
-intros 6;elim H
+lemma WFE_bound_bound : ∀x,T,U,G.G ⊢ ♦ → !x ⊴  T ∈ G → !x ⊴ U ∈ G → T = U.
+intros 5;elim H
   [lapply (not_in_list_nil ? ? H1);elim Hletin
   |elim (in_list_cons_case ? ? ? ? H6)
      [destruct H7;destruct;elim (in_list_cons_case ? ? ? ? H5)
@@ -295,9 +300,9 @@ intros 6;elim H
         |apply (H2 H8 H7)]]]
 qed.
 
-lemma WFT_to_incl: ∀G,T,U.(∀X.¬in_list ? X (fv_env G) → ¬in_list ? X (fv_type U) →
-    WFType (mk_bound true X T::G) (subst_type_nat U (TFree X) O))
-  → incl ? (fv_type U) (fv_env G).
+lemma WFT_to_incl: ∀G,T,U.(∀X.X ∉ fv_env G → X ∉ fv_type U →
+    (mk_bound true X T::G ⊢ (subst_type_nat U (TFree X) O))) →
+    fv_type U ⊆ fv_env G.
 intros;elim (fresh_name (fv_type U@fv_env G));lapply(H a)
   [unfold;intros;lapply (fv_WFT ? x ? Hletin)
      [simplify in Hletin1;inversion Hletin1;intros
@@ -308,11 +313,12 @@ intros;elim (fresh_name (fv_type U@fv_env G));lapply(H a)
 qed.
 
 lemma incl_fv_env: ∀X,G,G1,U,P.
-      incl ? (fv_env (G1@(mk_bound true X U::G))) 
-             (fv_env (G1@(mk_bound true X P::G))).
+      fv_env (G1@ !X ⊴ U::G) ⊆ fv_env (G1@ !X ⊴ P::G).
 intros.rewrite < fv_env_extends.apply incl_A_A.
 qed.
 
 lemma fv_append : ∀G,H.fv_env (G @ H) = fv_env G @ fv_env H.
-intro;elim G;simplify;autobatch paramodulation;
+intro;elim G;simplify;
+[reflexivity
+|elim a;simplify;elim b;simplify;lapply (H H1);rewrite > Hletin;reflexivity]
 qed.
\ No newline at end of file
diff --git a/helm/software/matita/contribs/POPLmark/Fsub/part1a.ma b/helm/software/matita/contribs/POPLmark/Fsub/part1a.ma
index f38b5b332..9e097b279 100644
--- a/helm/software/matita/contribs/POPLmark/Fsub/part1a.ma
+++ b/helm/software/matita/contribs/POPLmark/Fsub/part1a.ma
@@ -15,7 +15,7 @@
 include "Fsub/defn.ma".
 
 (*** Lemma A.1 (Reflexivity) ***)
-theorem JS_Refl : ∀T,G.WFType G T → WFEnv G → G ⊢ T ⊴  T.
+theorem JS_Refl : ∀T,G.(G ⊢ T) → G ⊢ ♦ → G ⊢ T ⊴  T.
 intros 3; elim H;
  [1,2,3: autobatch
  | apply SA_All; [ autobatch | intros;autobatch depth=4 size=10]]
@@ -27,7 +27,7 @@ qed.
  * set inclusion.
  *)
 
-lemma JS_weakening : ∀G,T,U.G ⊢ T ⊴ U → ∀H.WFEnv H → incl ? G H → H ⊢ T ⊴ U.
+lemma JS_weakening : ∀G,T,U.G ⊢ T ⊴ U → ∀H.H ⊢ ♦ → G ⊆ H → H ⊢ T ⊴ U.
 intros 4; elim H;
  [1,2,3,4: autobatch depth=4 size=7
  | apply (SA_All ? ? ? ? ? (H2 ? H6 H7));
@@ -38,14 +38,14 @@ inverter JS_indinv for JSubtype (%?%).
 
 theorem narrowing:∀X,G,G1,U,P,M,N.
   G1 ⊢ P ⊴ U → (∀G2,T.G2@G1 ⊢ U ⊴ T → G2@G1 ⊢ P ⊴ T) → G ⊢ M ⊴ N →
-  ∀l.G=l@(mk_bound true X U::G1) → l@(mk_bound true X P::G1) ⊢ M ⊴ N.
+  ∀l.G=l@ !X ⊴ U::G1 → l@ !X ⊴ P::G1 ⊢ M ⊴ N.
 intros 10.elim H2; destruct;
  [letin x \def fv_env. letin y ≝incl. autobatch depth=4 size=8.
  | autobatch depth=4 size=7;
  | elim (decidable_eq_nat X n)
     [apply (SA_Trans_TVar ? ? ? P); destruct;
       [ autobatch
-      | lapply (WFE_bound_bound true X t1 U ? ? H3); autobatch]
+      | lapply (WFE_bound_bound X t1 U ? ? H3); autobatch]
     | apply (SA_Trans_TVar ? ? ? t1); autobatch]
  | autobatch
  | apply SA_All;
@@ -53,8 +53,8 @@ intros 10.elim H2; destruct;
     | intros; apply (H6 ? ? (mk_bound true X1 t2::l1)); autobatch]]
 qed.
 
-lemma JS_trans_prova: ∀T,G1.WFType G1 T →
-∀G,R,U.incl ? (fv_env G1) (fv_env G) → G ⊢ R ⊴ T → G ⊢ T ⊴ U → G ⊢ R ⊴ U.
+lemma JS_trans_prova: ∀T,G1.(G1 ⊢ T) →
+      ∀G,R,U.fv_env G1 ⊆ fv_env G → G ⊢ R ⊴ T → G ⊢ T ⊴ U → G ⊢ R ⊴ U.
 intros 3;elim H;clear H;
   [elim H3 using JS_indinv;destruct;autobatch
   |inversion H3; intros; destruct; assumption
@@ -71,6 +71,7 @@ intros 3;elim H;clear H;
             [4: apply (narrowing X (mk_bound true X t::G) ? ? ? ? ? H11 ? ? [])
                [intros;apply H2;try unfold;intros;autobatch; 
                |*:autobatch]
+            |3:apply incl_cons;apply H5
             |*:autobatch]]]]]
 qed.
 
@@ -79,8 +80,8 @@ intros 5; apply (JS_trans_prova ? G); autobatch depth=2.
 qed.
 
 theorem JS_narrow : ∀G1,G2,X,P,Q,T,U.
-                       (G2 @ (mk_bound true X Q :: G1)) ⊢ T ⊴ U → G1 ⊢ P ⊴ Q →
-                       (G2 @ (mk_bound true X P :: G1)) ⊢ T ⊴ U.
+                       G2 @ !X ⊴ Q :: G1 ⊢ T ⊴ U → G1 ⊢ P ⊴ Q →
+                       G2 @ !X ⊴ P :: G1 ⊢ T ⊴ U.
 intros;apply (narrowing ? ? ? ? ? ? ? H1 ? H) [|autobatch]
 intros;apply (JS_trans ? ? ? ? ? H2);apply (JS_weakening ? ? ? H1);autobatch.
 qed.
diff --git a/helm/software/matita/contribs/POPLmark/Fsub/util.ma b/helm/software/matita/contribs/POPLmark/Fsub/util.ma
index d3f4dc023..47b95a69e 100644
--- a/helm/software/matita/contribs/POPLmark/Fsub/util.ma
+++ b/helm/software/matita/contribs/POPLmark/Fsub/util.ma
@@ -43,16 +43,284 @@ apply (leb_elim m n)
   ]
 qed.  
 
-(*
-notation > "hvbox(x ∈ l)"
-  non associative with precedence 30 for @{ 'inlist $x $l }.
-notation < "hvbox(x \nbsp ∈ \nbsp l)"
-  non associative with precedence 30 for @{ 'inlist $x $l }.
-*)  
-interpretation "item in list" 'mem x l = (in_list ? x l).
-
 lemma max_case : \forall m,n.(max m n) = match (leb m n) with
       [ true \Rightarrow n
       | false \Rightarrow m ].
 intros;elim m;simplify;reflexivity;
 qed.
+
+definition swap : nat → nat → nat → nat ≝
+  λu,v,x.match (eqb x u) with
+    [true ⇒ v
+    |false ⇒ match (eqb x v) with
+       [true ⇒ u
+       |false ⇒ x]].
+       
+lemma swap_left : ∀x,y.(swap x y x) = y.
+intros;unfold swap;rewrite > eqb_n_n;simplify;reflexivity;
+qed.
+
+lemma swap_right : ∀x,y.(swap x y y) = x.
+intros;unfold swap;rewrite > eqb_n_n;apply (eqb_elim y x);intro;autobatch;
+qed.
+
+lemma swap_other : \forall x,y,z.(z \neq x) \to (z \neq y) \to (swap x y z) = z.
+intros;unfold swap;apply (eqb_elim z x);intro;simplify
+  [elim H;assumption
+  |rewrite > not_eq_to_eqb_false;autobatch]
+qed.
+
+lemma swap_inv : \forall u,v,x.(swap u v (swap u v x)) = x.
+intros;unfold in match (swap u v x);apply (eqb_elim x u);intro;simplify
+  [autobatch paramodulation
+  |apply (eqb_elim x v);intro;simplify
+     [autobatch paramodulation
+     |apply swap_other;assumption]]
+qed.
+
+lemma swap_inj : ∀u,v,x,y.swap u v x = swap u v y → x = y.
+intros 4;unfold swap;apply (eqb_elim x u);simplify;intro
+  [apply (eqb_elim y u);simplify;intro
+     [intro;autobatch paramodulation
+     |apply (eqb_elim y v);simplify;intros
+        [autobatch paramodulation
+        |elim H2;symmetry;assumption]]
+  |apply (eqb_elim y u);simplify;intro
+     [apply (eqb_elim x v);simplify;intros;
+        [autobatch paramodulation
+        |elim H2;assumption]
+     |apply (eqb_elim x v);simplify;intro
+        [apply (eqb_elim y v);simplify;intros
+           [autobatch paramodulation
+           |elim H1;symmetry;assumption]
+        |apply (eqb_elim y v);simplify;intros
+           [elim H;assumption
+           |assumption]]]]
+qed.
+
+definition swap_list : nat \to nat \to (list nat) \to (list nat) ≝
+  \lambda u,v,l.(map ? ? (swap u v) l). 
+
+let rec posn l x on l ≝
+  match l with
+  [ nil ⇒ O
+  | (cons (y:nat) l2) ⇒
+      match (eqb x y) with
+            [ true ⇒ O
+            | false ⇒ S (posn l2 x)]].
+            
+let rec lookup n l on l ≝
+  match l with
+    [ nil ⇒ false
+    | cons (x:nat) l1 ⇒ match (eqb n x) with
+              [true ⇒ true
+              |false ⇒ (lookup n l1)]]. 
+                             
+let rec head (A:Type) l on l ≝
+  match l with
+  [ nil ⇒ None A
+  | (cons (x:A) l2) ⇒ Some A x].
+
+definition max_list : (list nat) \to nat \def
+  \lambda l.let rec aux l0 m on l0 \def
+    match l0 with
+      [ nil ⇒ m
+      | (cons n l2) ⇒ (aux l2 (max m n))]
+    in aux l O.
+
+let rec remove_nat (x:nat) (l:list nat) on l \def
+  match l with
+  [ nil ⇒ (nil nat) 
+  | (cons y l2) ⇒ match (eqb x y) with
+                  [ true ⇒ (remove_nat x l2)
+                  | false ⇒ (y :: (remove_nat x l2)) ]].
+                  
+lemma in_lookup : \forall x,l.x ∈ l \to (lookup x l = true).
+intros;elim H;simplify
+  [rewrite > eqb_n_n;reflexivity
+  |rewrite > H2;elim (eqb a a1);reflexivity]
+qed.
+
+lemma lookup_in : \forall x,l.(lookup x l = true) \to x ∈ l.
+intros 2;elim l
+  [simplify in H;destruct H
+  |generalize in match H1;simplify;elim (decidable_eq_nat x a)
+     [applyS in_list_head
+     |apply in_list_cons;apply H;
+      rewrite > (not_eq_to_eqb_false ? ? H2) in H3;simplify in H3;assumption]]
+qed.
+
+lemma posn_length : \forall x,vars.x ∈ vars → 
+                       (posn vars x) < (length ? vars).
+intros 2;elim vars
+  [elim (not_in_list_nil ? ? H)
+  |inversion H1;intros;destruct;simplify
+     [rewrite > eqb_n_n;simplify;
+      apply lt_O_S
+     |elim (eqb x a);simplify
+        [apply lt_O_S
+        |apply le_S_S;apply H;assumption]]]
+qed.
+
+lemma in_remove : \forall a,b,l.(a ≠ b) \to a ∈ l \to
+                                a ∈ (remove_nat b l).
+intros 4;elim l
+  [elim (not_in_list_nil ? ? H1)
+  |inversion H2;intros;destruct;simplify
+     [rewrite > not_eq_to_eqb_false
+        [simplify;apply in_list_head
+        |intro;apply H;symmetry;assumption]
+     |elim (eqb b a1);simplify
+        [apply H1;assumption
+        |apply in_list_cons;apply H1;assumption]]]
+qed.
+
+lemma swap_same : \forall x,y.swap x x y = y.
+intros;elim (decidable_eq_nat y x)
+  [autobatch paramodulation
+  |rewrite > swap_other;autobatch]
+qed.
+
+lemma not_nat_in_to_lookup_false : ∀l,X. X ∉ l → lookup X l = false.
+intros 2;elim l;simplify
+  [reflexivity
+  |elim (decidable_eq_nat X a)
+     [elim H1;rewrite > H2;apply in_list_head
+     |rewrite > (not_eq_to_eqb_false ? ? H2);simplify;apply H;intro;apply H1;
+      apply (in_list_cons ? ? ? ? H3);]]
+qed.
+
+lemma lookup_swap : ∀a,b,x,vars.
+                    lookup (swap a b x) (swap_list a b vars) =
+                    lookup x vars.
+intros 4;elim vars;simplify
+  [reflexivity
+  |elim (decidable_eq_nat x a1)
+     [rewrite > H1;rewrite > eqb_n_n;rewrite > eqb_n_n;simplify;reflexivity
+     |rewrite > (not_eq_to_eqb_false ? ? H1);elim (decidable_eq_nat x a)
+        [rewrite > H;rewrite > H2;rewrite > swap_left;
+         elim (decidable_eq_nat b a1)
+           [rewrite < H3;rewrite > swap_right;
+            rewrite > (not_eq_to_eqb_false b a)
+              [reflexivity
+              |intro;autobatch]
+           |rewrite > (swap_other a b a1)
+              [rewrite > (not_eq_to_eqb_false ? ? H3);simplify;reflexivity
+              |*:intro;autobatch]]
+        |elim (decidable_eq_nat x b)
+           [rewrite > H;rewrite > H3;rewrite > swap_right;
+            elim (decidable_eq_nat a1 a)
+              [rewrite > H4;rewrite > swap_left;
+               rewrite > (not_eq_to_eqb_false a b)
+                 [reflexivity
+                 |intro;autobatch]
+              |rewrite > (swap_other a b a1)
+                 [rewrite > (not_eq_to_eqb_false a a1)
+                    [reflexivity
+                    |intro;autobatch]
+                 |assumption
+                 |intro;autobatch]]
+           |rewrite > H;rewrite > (swap_other a b x)
+              [elim (decidable_eq_nat a a1)
+                 [rewrite > H4;rewrite > swap_left;
+                  rewrite > (not_eq_to_eqb_false ? ? H3);reflexivity
+                 |elim (decidable_eq_nat b a1)
+                    [rewrite > H5;rewrite > swap_right;
+                     rewrite > (not_eq_to_eqb_false ? ? H2);reflexivity
+                    |rewrite > (swap_other a b a1)
+                       [rewrite > (not_eq_to_eqb_false ? ? H1);reflexivity
+                       |*:intro;autobatch]]]
+              |*:assumption]]]]]
+qed.
+
+lemma posn_swap : ∀a,b,x,vars.
+                  posn vars x = posn (swap_list a b vars) (swap a b x).
+intros 4;elim vars;simplify
+  [reflexivity
+  |rewrite < H;elim (decidable_eq_nat x a1)
+     [rewrite > H1;do 2 rewrite > eqb_n_n;reflexivity
+     |elim (decidable_eq_nat (swap a b x) (swap a b a1))
+        [elim H1;autobatch
+        |rewrite > (not_eq_to_eqb_false ? ? H1);
+         rewrite > (not_eq_to_eqb_false ? ? H2);reflexivity]]]
+qed.
+
+lemma remove_inlist : \forall x,y,l.x ∈ (remove_nat y l) → x ∈ l \land x ≠ y.
+intros 3;elim l 0;simplify;intro
+  [elim (not_in_list_nil ? ? H)
+  |elim (decidable_eq_nat y a)
+     [rewrite > H in H2;rewrite > eqb_n_n in H2;simplify in H2;
+      rewrite > H in H1;elim (H1 H2);rewrite > H;split
+        [apply in_list_cons;assumption
+        |assumption]
+     |rewrite > (not_eq_to_eqb_false ? ? H) in H2;simplify in H2;
+      inversion H2;intros;destruct;
+        [split;autobatch
+        |elim (H1 H3);split;autobatch]]]
+qed.
+
+lemma inlist_remove : ∀x,y,l.x ∈ l → x ≠ y → x ∈ (remove_nat y l).
+intros 3;elim l
+  [elim (not_in_list_nil ? ? H);
+  |simplify;elim (decidable_eq_nat y a)
+     [rewrite > (eq_to_eqb_true ? ? H3);simplify;apply H
+        [inversion H1;intros;destruct;
+           [elim H2;reflexivity
+           |assumption]
+        |assumption]
+     |rewrite > (not_eq_to_eqb_false ? ? H3);simplify;
+      inversion H1;intros;destruct;autobatch]]
+qed.
+
+lemma swap_case: ∀u,v,x.(swap u v x) = u ∨ (swap u v x) = v ∨ (swap u v x = x).
+intros;unfold in match swap;simplify;elim (eqb x u);simplify
+  [autobatch
+  |elim (eqb x v);simplify;autobatch]
+qed.
+    
+definition distinct_list ≝
+λl.∀n,m.n < length ? l → m < length ? l → n ≠ m → nth ? l O n ≠ nth ? l O m.
+
+lemma posn_nth: ∀l,n.distinct_list l → n < length ? l → 
+                    posn l (nth ? l O n) = n.
+intro;elim l
+  [simplify in H1;elim (not_le_Sn_O ? H1)
+  |simplify in H2;generalize in match H2;elim n
+     [simplify;rewrite > eqb_n_n;simplify;reflexivity
+     |simplify;cut (nth ? (a::l1) O (S n1) ≠ nth ? (a::l1) O O)
+        [simplify in Hcut;rewrite > (not_eq_to_eqb_false ? ? Hcut);simplify;
+         rewrite > (H n1)
+           [reflexivity
+           |unfold;intros;unfold in H1;lapply (H1 (S n2) (S m));
+              [simplify in Hletin;assumption
+              |2,3:simplify;autobatch
+              |intro;apply H7;destruct H8;reflexivity]
+           |autobatch]
+        |intro;apply H1;
+           [6:apply H5
+           |skip
+           |skip
+           |(*** *:autobatch; *)
+            apply H4
+           |simplify;autobatch
+           |intro;elim (not_eq_O_S n1);symmetry;assumption]]]]
+qed.
+
+lemma nth_in_list : ∀l,n. n < length ? l → (nth ? l O n) ∈ l.
+intro;elim l
+  [simplify in H;elim (not_le_Sn_O ? H)
+  |generalize in match H1;elim n;simplify
+     [apply in_list_head
+     |apply in_list_cons;apply H;simplify in H3;apply (le_S_S_to_le ? ? H3)]]
+qed.
+
+lemma lookup_nth : \forall l,n.n < length ? l \to 
+                   lookup (nth nat l O n) l = true.
+intro;elim l
+  [elim (not_le_Sn_O ? H);
+  |generalize in match H1;elim n;simplify
+     [rewrite > eqb_n_n;reflexivity
+     |elim (eqb (nth nat l1 O n1) a);simplify;
+        [reflexivity
+        |apply H;apply le_S_S_to_le;assumption]]]
+qed.
\ No newline at end of file