X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FPOPLmark%2FFsub%2Fadeq.ma;h=2a0f730abdc5b307c4675601ab1ad3e9f93452cf;hb=964844c87f7c3d7061dfeb7f2d84b6b8bbcdaf13;hp=056a5105b8d6cca87edfa2a88bb346e751c71b97;hpb=3fb8cc2606e15f256f93c653b5136f609b385208;p=helm.git

diff --git a/helm/software/matita/contribs/POPLmark/Fsub/adeq.ma b/helm/software/matita/contribs/POPLmark/Fsub/adeq.ma
index 056a5105b..2a0f730ab 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,52 @@ 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 ∈ (fv_NTyp U) → Y = X) → 
                     (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
               (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 ∈ (fv_NTyp S2) → Z = X) →
+                  (Z ∈ (fv_NTyp T2) → Z = Y) →
               (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
@@ -264,12 +135,25 @@ let rec nt_len T \def
 definition encodeenv : list nbound → list bound ≝
   map nbound bound 
     (λb.match b with
-       [ mk_nbound b x T ⇒ mk_bound b x (encodetype T []) ]).
+       [ mk_nbound b x T ⇒ mk_bound b x (encodetype T []) ]). 
        
+notation < "⌈ T ⌉ \sub l" with precedence 25 for @{'encode2 $T $l}.
+interpretation "Fsub names to LN type encoding" 'encode2 T l = (encodetype T l).
+notation < "⌈ G ⌉" with precedence 25 for @{'encode $G}.
+interpretation "Fsub names to LN env encoding" 'encode G = (encodeenv G).
+notation < "| T |" with precedence 25 for @{'abs $T}.
+interpretation "Fsub named type length" 'abs T = (nt_len T).
+interpretation "list length" 'abs l = (length ? l).
+notation < "〈a,b〉 · T" with precedence 60 for @{'swap $a $b $T}.
+interpretation "natural swap" 'swap a b n = (swap a b n).
+interpretation "Fsub name swap in a named type" 'swap a b T = (swap_NTyp a b T).
+interpretation "Fsub name swap in a LN type" 'swap a b T = (swap_Typ a b T).
+interpretation "natural list swap" 'swap a b l = (swap_list a b l).
+
 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 +197,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 +206,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 +268,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 +302,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 +379,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 +398,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 +406,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 +444,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 +480,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 +561,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 +572,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 +585,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 +616,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 +635,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 +647,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 +664,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 +677,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 +710,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 +787,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 +830,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,23 +848,17 @@ 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]]
   |intro;autobatch depth=4
-  |right;intro;autobatch depth=5]]]
+  |intro;elim H7;autobatch]]]
 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)
@@ -1261,11 +889,8 @@ intros;elim H;simplify
   [simplify in H4;apply H4
    [rewrite > (eq_fv_Nenv_fv_env l);assumption
    |elim (decidable_eq_nat X n)
-    [left;assumption
-    |right;intro;apply H6;apply (fv_NTyp_fv_Typ ? ? ? H8);intro;
-     apply H7;inversion H9;intros;destruct;
-     [reflexivity
-     |elim (not_in_list_nil ? ? H10)]]]
+    [assumption
+    |elim H6;apply (fv_NTyp_fv_Typ ??? H8);autobatch]]
   |4:intro;elim (decidable_eq_nat X n)
    [assumption
    |elim H6;cut (¬(in_list ? X [n]))
@@ -1291,8 +916,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 +925,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)
@@ -1320,6 +945,18 @@ intro;elim T;simplify;unfold;
         |autobatch]]]
 qed.
 
+lemma decidable_inlist_nat : ∀l:list nat.∀n.decidable (n ∈ l).
+intros;elim l
+[right;autobatch
+|elim H
+ [left;autobatch
+ |elim (decidable_eq_nat n a)
+  [left;autobatch
+  |right;intro;apply H2;inversion H3;intros;destruct;
+   [reflexivity
+   |elim (H1 H4)]]]]
+qed.
+
 lemma adeq_WFT2 : ∀G1,T1.WFType G1 T1 → 
                      ∀G2,T2.G1 = encodeenv G2 → T1 = encodetype T2 [] → 
                    NWFType G2 T2.
@@ -1353,28 +990,26 @@ intros 3;elim H
    elim Hcut;elim H7;elim H8;clear Hcut H7 H8;rewrite > H9;
    rewrite > H9 in H6;simplify in H6;destruct;apply NWFT_Forall
      [autobatch
-     |intros;elim H6
-        [rewrite > H7;cut (swap_NTyp a a a2 = a2) 
-           [|elim a2;simplify;autobatch]
-         rewrite > Hcut;apply (H4 Y)
-           [4:rewrite > H7;(*** autobatch *)
-            change in ⊢ (? ? (? (? ? %) ? ?) ?) with ([]@[a]);
-            symmetry;rewrite < Hcut in ⊢ (??%?);
-            change in ⊢ (? ? ? (? ? ? %)) with (length nat []);autobatch
-           |*:autobatch]
-        |apply (H4 Y)
-           [1,3:autobatch
-           |intro;autobatch
-           |symmetry;apply (encode_subst a2 Y a []);
-              [3:intro;elim (H7 H8)
-              |*:autobatch]]]]
+     |intros;elim (decidable_inlist_nat (fv_NTyp a2) Y)
+      [lapply (H6 H7) as H8;rewrite > H8;rewrite > (? : swap_NTyp a a a2 = a2)
+       [apply (H4 Y)
+        [4:rewrite > H8;change in ⊢ (?? (? (??%) ??) ?) with ([]@[a]);
+         symmetry;change in ⊢ (??? (???%)) with (length nat []);autobatch
+        |*:autobatch]
+       |elim a2;simplify;autobatch]
+      |apply (H4 Y)
+       [1,3:autobatch
+       |intro;autobatch
+       |symmetry;apply (encode_subst a2 Y a [])
+        [3:intro;elim (H7 H8)
+        |*:autobatch]]]]
 qed.
 
 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,63 +1017,199 @@ 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.
 
-lemma NJSubtype_to_NWFT : ∀G,T,U.NJSubtype G T U → NWFType G T ∧ NWFType G U.
-intros;elim H
-  [1,2:split;autobatch
-  |elim H3;split; 
-     [apply NWFT_TName;elim l in H1
-        [elim (not_in_list_nil ? ? H1)
-        |inversion H6;intros;destruct;
-           [simplify;autobatch
-           |elim a;simplify;autobatch]]
-     |assumption]
-  |elim H2;elim H4;split;autobatch
-  |split;assumption
-  |elim H2;split
-     [lapply (adeq_WFT ? ? H5);autobatch;
-     |lapply (adeq_WFT ? ? H6);autobatch]]
+lemma NJS_fv_to_fvNenv : ∀G,T,U.NJSubtype G T U → 
+  fv_NTyp T ⊆ fv_Nenv G ∧ fv_NTyp U ⊆ fv_Nenv G.
+intros;elim H;simplify;
+[split
+ [autobatch
+ |unfold;intros;elim (not_in_list_nil ?? H3)]
+|split;unfold;intros;rewrite > (in_list_singleton_to_eq ??? H3);assumption
+|decompose;split;try autobatch;unfold;intros;
+ rewrite > (in_list_singleton_to_eq ??? H3);
+ generalize in match (refl_eq ? (mk_nbound true n n2));
+ elim H1 in ⊢ (???% → %)
+ [rewrite < H6;simplify;apply in_list_head
+ |cases a1;cases b;simplify;
+  [apply in_list_cons;apply H7;assumption
+  |apply H7;assumption]]
+|decompose;split;unfold;intros;
+ [elim (in_list_append_to_or_in_list ???? H4);autobatch
+ |elim (in_list_append_to_or_in_list ???? H4);autobatch]
+|decompose;split;unfold;intros;
+ [elim (in_list_append_to_or_in_list ? ? ? ? H2)
+  [autobatch
+  |elim (fresh_name (x::fv_Nenv l@var_NTyp n3@var_NTyp n5));lapply (H4 a)
+   [cut (a ≠ x ∧ x ≠ n)
+    [elim Hcut;elim Hletin;lapply (H11 x)
+     [simplify in Hletin1;inversion Hletin1;intros;destruct;
+      [elim Hcut;elim H13;reflexivity
+      |assumption]
+     |elim n3 in H7 H8
+      [simplify in H7;elim (decidable_eq_nat n n6)
+       [rewrite > (eq_to_eqb_true ? ? H13) in H7;simplify in H7;
+        elim (not_in_list_nil ? ? H7)
+       |rewrite > (not_eq_to_eqb_false ? ? H13) in H7;
+        simplify in H7;inversion H7;intros
+        [destruct;simplify;rewrite > swap_other
+         [apply in_list_head
+         |intro;apply H8;rewrite > H14;autobatch
+         |intro;apply H13;rewrite > H14;reflexivity]
+        |destruct;elim (not_in_list_nil ? ? H14)]]
+      |simplify in H7;elim (not_in_list_nil ? ? H7)
+      |simplify in H14;simplify;elim (remove_inlist ? ? ? H13);
+       simplify in H15;elim (in_list_append_to_or_in_list ? ? ? ? H15)
+       [apply in_list_to_in_list_append_l;apply H7
+        [apply (in_remove ? ? ? H16 H17)
+        |intro;apply H14;simplify;
+         rewrite < (associative_append ? [x] (fv_Nenv l) ((var_NTyp n6 @ var_NTyp n7)@var_NTyp n5));
+         elim (in_list_append_to_or_in_list ? ? (x::fv_Nenv l) (var_NTyp n6@var_NTyp n5) H18);
+         [apply in_list_to_in_list_append_l;apply H19
+         |apply in_list_to_in_list_append_r;
+          elim (in_list_append_to_or_in_list ???? H19);autobatch]]
+       |apply in_list_to_in_list_append_r;apply H8
+        [apply (in_remove ? ? ? H16 H17)
+        |intro;apply H14;simplify;
+         rewrite < (associative_append ? [x] (fv_Nenv l) ((var_NTyp n6 @ var_NTyp n7)@var_NTyp n5));
+         elim (in_list_append_to_or_in_list ? ? (x::fv_Nenv l) (var_NTyp n7@var_NTyp n5) H18);
+         [apply in_list_to_in_list_append_l;apply H19
+         |apply in_list_to_in_list_append_r;
+          elim (in_list_append_to_or_in_list ???? H19);autobatch]]]
+      |simplify in H14;simplify;elim (remove_inlist ? ? ? H13);
+       simplify in H15;elim (in_list_append_to_or_in_list ? ? ? ? H15)
+       [apply in_list_to_in_list_append_l;apply H7
+        [apply (in_remove ? ? ? H16 H17)
+        |intro;apply H14;simplify;
+         rewrite < (associative_append ? [x] (fv_Nenv l) (n6::(var_NTyp n7 @ var_NTyp n8)@var_NTyp n5));
+         elim (in_list_append_to_or_in_list ? ? (x::fv_Nenv l) (var_NTyp n7@var_NTyp n5) H18);
+         [apply in_list_to_in_list_append_l;apply H19
+         |apply in_list_to_in_list_append_r;apply in_list_cons;
+          elim (in_list_append_to_or_in_list ???? H19);autobatch]]
+       |apply in_list_to_in_list_append_r;apply in_remove;
+        [elim (remove_inlist ??? H13);intro;apply H19;
+         elim (swap_case a n n6)
+         [elim H21
+          [elim H14;rewrite < H22;rewrite < H20;apply in_list_head
+          |autobatch paramodulation]
+         |elim (remove_inlist ??? H17);elim H23;autobatch paramodulation]
+        |apply H8
+         [apply (in_remove ? ? ? H16);elim (remove_inlist ??? H17);assumption
+         |intro;apply H14;simplify;
+          rewrite < (associative_append ? [x] (fv_Nenv l) (n6::(var_NTyp n7 @ var_NTyp n8)@var_NTyp n5));
+          elim (in_list_append_to_or_in_list ? ? (x::fv_Nenv l) (var_NTyp n8@var_NTyp n5) H18);
+          [apply in_list_to_in_list_append_l;apply H19
+          |apply in_list_to_in_list_append_r;apply in_list_cons;
+           elim (in_list_append_to_or_in_list ???? H19);autobatch]]]]]]
+    |split
+     [intro;apply H8;rewrite > H9;apply in_list_head
+     |elim (remove_inlist ? ? ? H7);assumption]]
+   |intro;autobatch depth=4
+   |3,4:intro;elim H8;apply in_list_cons;autobatch depth=4]]
+ |elim (in_list_append_to_or_in_list ? ? ? ? H2)
+  [autobatch
+  |elim (fresh_name (x::fv_Nenv l@var_NTyp n3@var_NTyp n5));lapply (H4 a)
+   [cut (a ≠ x ∧ x ≠ n1)
+    [elim Hcut;elim Hletin;lapply (H12 x)
+     [simplify in Hletin1;inversion Hletin1;intros;destruct;
+      [elim Hcut;elim H13;reflexivity
+      |assumption]
+     |elim n5 in H7 H8
+      [simplify in H7;elim (decidable_eq_nat n1 n6)
+       [rewrite > (eq_to_eqb_true ? ? H13) in H7;simplify in H7;
+        elim (not_in_list_nil ? ? H7)
+       |rewrite > (not_eq_to_eqb_false ? ? H13) in H7;
+        simplify in H7;inversion H7;intros
+        [destruct;simplify;rewrite > swap_other
+         [apply in_list_head
+         |intro;apply H8;rewrite > H14;autobatch
+         |intro;apply H13;rewrite > H14;reflexivity]
+        |destruct;elim (not_in_list_nil ? ? H14)]]
+      |simplify in H7;elim (not_in_list_nil ? ? H7)
+      |simplify in H14;simplify;elim (remove_inlist ? ? ? H13);
+       simplify in H15;elim (in_list_append_to_or_in_list ? ? ? ? H15)
+       [apply in_list_to_in_list_append_l;apply H7
+        [apply (in_remove ? ? ? H16 H17)
+        |intro;apply H14;simplify;
+         rewrite < (associative_append ? [x] (fv_Nenv l) (var_NTyp n3 @ var_NTyp n6@var_NTyp n7));
+         elim (in_list_append_to_or_in_list ? ? (x::fv_Nenv l) (var_NTyp n3@var_NTyp n6) H18);
+         [apply in_list_to_in_list_append_l;apply H19
+         |apply in_list_to_in_list_append_r;
+          elim (in_list_append_to_or_in_list ???? H19);autobatch]]
+       |apply in_list_to_in_list_append_r;apply H8
+        [apply (in_remove ? ? ? H16 H17)
+        |intro;apply H14;simplify;
+         rewrite < (associative_append ? [x] (fv_Nenv l) (var_NTyp n3 @ var_NTyp n6@var_NTyp n7));
+         elim (in_list_append_to_or_in_list ? ? (x::fv_Nenv l) (var_NTyp n3@var_NTyp n7) H18);
+         [apply in_list_to_in_list_append_l;apply H19
+         |apply in_list_to_in_list_append_r;
+          elim (in_list_append_to_or_in_list ???? H19);autobatch]]]
+      |simplify in H14;simplify;elim (remove_inlist ? ? ? H13);
+       simplify in H15;elim (in_list_append_to_or_in_list ? ? ? ? H15)
+       [apply in_list_to_in_list_append_l;apply H7
+        [apply (in_remove ? ? ? H16 H17)
+        |intro;apply H14;simplify;
+         rewrite < (associative_append ? [x] (fv_Nenv l) (var_NTyp n3@n6::var_NTyp n7 @ var_NTyp n8));
+         elim (in_list_append_to_or_in_list ? ? (x::fv_Nenv l) (var_NTyp n3@var_NTyp n7) H18);
+         [apply in_list_to_in_list_append_l;apply H19
+         |apply in_list_to_in_list_append_r;
+          elim (in_list_append_to_or_in_list ???? H19);autobatch depth=4]]
+       |apply in_list_to_in_list_append_r;apply in_remove;
+        [elim (remove_inlist ??? H13);intro;apply H19;
+         elim (swap_case a n1 n6)
+         [elim H21
+          [elim H14;rewrite < H22;rewrite < H20;apply in_list_head
+          |autobatch paramodulation]
+         |elim (remove_inlist ??? H17);elim H23;autobatch paramodulation]
+        |apply H8
+         [apply (in_remove ? ? ? H16);elim (remove_inlist ??? H17);assumption
+         |intro;apply H14;simplify;
+          rewrite < (associative_append ? [x] (fv_Nenv l) (var_NTyp n3@n6::var_NTyp n7 @ var_NTyp n8));
+          elim (in_list_append_to_or_in_list ? ? (x::fv_Nenv l) (var_NTyp n3@var_NTyp n8) H18);
+          [apply in_list_to_in_list_append_l;apply H19
+          |apply in_list_to_in_list_append_r;
+           elim (in_list_append_to_or_in_list ???? H19);autobatch depth=4]]]]]]
+    |split
+     [intro;apply H8;rewrite > H9;apply in_list_head
+     |elim (remove_inlist ? ? ? H7);assumption]]
+   |intro;autobatch depth=4
+   |3,4:intro;elim H8;apply in_list_cons;autobatch depth=4]]]]
 qed.
-
+ 
 theorem adequacy : ∀G,T,U.NJSubtype G T U → 
                     JSubtype (encodeenv G) (encodetype T []) (encodetype U []).
 intros;elim H;simplify
   [1,2,3,4:autobatch
   |apply SA_All
      [assumption
-     |intros;lapply (NSA_All ? ? ? ? ? ? ? H1 H2 H3 H5);
+     |intros;lapply (NSA_All ? ? ? ? ? ? ? H1 H3);
       rewrite < (encode_subst n3 X n [])
         [rewrite < (encode_subst n5 X n1 [])
-           [rewrite < eq_fv_Nenv_fv_env in H7;
-            elim (NJSubtype_to_NWFT ? ? ? Hletin);
-            lapply (in_fvNTyp_in_fvNenv ? ? H8);
-            lapply (in_fvNTyp_in_fvNenv ? ? H9);
-            simplify in Hletin1;simplify in Hletin2;
-            apply (H6 ? H7)
+           [rewrite < eq_fv_Nenv_fv_env in H5;
+            elim (NJS_fv_to_fvNenv ? ? ? Hletin);
+            simplify in H6;simplify in H7;
+            apply (H4 ? H5)
               [elim (decidable_eq_nat X n)
-                 [left;assumption
-                 |right;intro;lapply (in_remove ? ? ? H10 H11);elim H7;
-                  autobatch]
+                 [assumption
+                 |elim H5;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
-           |intro;elim (NJSubtype_to_NWFT ? ? ? Hletin);
-            lapply (in_fvNTyp_in_fvNenv ? ? H10);simplify in Hletin1;
+                 [assumption
+                 |elim H5;autobatch depth=5]]
+           |2,3:autobatch
+           |intro;elim (NJS_fv_to_fvNenv ? ? ? Hletin);
+            simplify in H8;
             elim (decidable_eq_nat X n1)
               [assumption
-              |lapply (in_remove ? ? ? H11 H8);elim H7;autobatch]]
+              |elim H5;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)
+        |intro;elim (NJS_fv_to_fvNenv ? ? ? Hletin);
+         simplify in H7;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 H5;autobatch depth=4]]]]
 qed.
 
 let rec closed_type T n ≝
@@ -1449,58 +1220,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 +1303,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 +1315,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 +1383,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)
@@ -1679,7 +1400,7 @@ intros 4;elim H 0
       destruct;lapply (SA_All ? ? ? ? ? H1 H3);
       lapply (JS_to_WFT1 ? ? ? Hletin);lapply (JS_to_WFT2 ? ? ? Hletin);
       apply NSA_All
-        [1,2,3:autobatch;
+        [autobatch;
         |intros;apply H4;
            [apply Z
            |2,3:autobatch
@@ -1696,9 +1417,7 @@ intros 4;elim H 0
                        |intro;autobatch]]]]
            |rewrite < (encode_subst a5 Z a3 [])
               [1,2,3:autobatch
-              |intro;elim H7
-                 [assumption
-                 |elim (H9 H8)]]]]
+              |intro;elim H7;autobatch]]]
      |generalize in match H6;elim T2 0;simplify;intros;destruct;
       generalize in match H7;elim U2 0;simplify;intros;destruct;
       autobatch depth=8 width=2 size=9]]