matita/contribs/POPLmark/Fsub/adeq.ma

   1
   2 (**************************************************************************)
   3 (*       ___                                                              *)
   4 (*      ||M||                                                             *)
   5 (*      ||A||       A project by Andrea Asperti                           *)
   6 (*      ||T||                                                             *)
   7 (*      ||I||       Developers:                                           *)
   8 (*      ||T||         The HELM team.                                      *)
   9 (*      ||A||         http://helm.cs.unibo.it                             *)
  10 (*      \   /                                                             *)
  11 (*       \ /        This file is distributed under the terms of the       *)
  12 (*        v         GNU General Public License Version 2                  *)
  13 (*                                                                        *)
  14 (**************************************************************************)
  15
  16 include "logic/equality.ma".
  17 include "nat/nat.ma".
  18 include "datatypes/bool.ma".
  19 include "list/list.ma".
  20 include "nat/compare.ma".
  21 include "Fsub/util.ma".
  22 include "Fsub/defn2.ma".
  23
  24 inductive NTyp : Set \def
  25 | TName : nat \to NTyp
  26 | NTop : NTyp
  27 | NArrow : NTyp \to NTyp \to NTyp
  28 | NForall : nat \to NTyp \to NTyp \to NTyp.
  29
  30 (*inductive NTerm : Set \def
  31 | Name : nat \to NTerm
  32 | NAbs : nat \to NTyp \to NTerm \to NTerm
  33 | NApp : NTerm \to NTerm \to NTerm
  34 | NTAbs : nat \to NTyp \to NTerm \to NTerm
  35 | NTApp : NTerm \to NTyp \to NTerm.*)
  36
  37 (*inductive LNTyp: nat \to Set \def
  38 | LNTVar : \forall m,n.(m < n) \to LNTyp n
  39 | LNTFree : \forall n.nat \to LNTyp n
  40 | LNTop : \forall n.LNTyp n
  41 | LNArrow : \forall n.(LNTyp n) \to (LNTyp n) \to (LNTyp n)
  42 | LNForall : \forall n.(LNTyp n) \to (LNTyp (S n)) \to (LNTyp n).
  43
  44 inductive LNTerm : nat \to Set \def
  45 | LNVar : \forall m,n.(m < n) \to LNTerm n
  46 | LNFree : \forall n.nat \to LNTerm n
  47 | LNAbs : \forall n.(LNTyp n) \to (LNTerm (S n)) \to (LNTerm n)
  48 | LNApp : \forall n.(LNTerm n) \to (LNTerm n) \to (LNTerm n)
  49 | LNTAbs : \forall n.(LNTyp n) \to (LNTerm (S n)) \to (LNTerm n)
  50 | LNTApp : \forall n.(LNTerm n) \to (LNTyp n) \to (LNTerm n).*)
  51
  52 record nbound : Set \def {
  53                            nistype : bool;
  54                            nname : nat;
  55                            nbtype : NTyp
  56                          }.
  57
  58 (*record lnbound (n:nat) : Set \def {
  59                            lnistype : bool;
  60                            lnname : nat;
  61                            lnbtype : LNTyp n
  62                          }.*)
  63
  64 inductive option (A:Type) : Set \def
  65 | Some : A \to option A
  66 | None : option A.
  67
  68 (*definition S_opt : (option nat) \to (option nat) \def
  69   \lambda n.match n with
  70   [ (Some n) \Rightarrow (Some nat (S n))
  71   | None \Rightarrow None nat].*)
  72
  73 (* position of the first occurrence of nat x in list l
  74    returns (length l) when x not in l *)
  75
  76 definition swap : nat \to nat \to nat \to nat \def
  77   \lambda u,v,x.match (eqb x u) with
  78     [true \Rightarrow v
  79     |false \Rightarrow match (eqb x v) with
  80        [true \Rightarrow u
  81        |false \Rightarrow x]].
  82
  83 axiom swap_left : \forall x,y.(swap x y x) = y.
  84 (*intros;unfold swap;rewrite > eqb_n_n;simplify;reflexivity;
  85 qed.*)
  86
  87 axiom swap_right : \forall x,y.(swap x y y) = x.
  88 (*intros;unfold swap;elim (eq_eqb_case y x)
  89   [elim H;rewrite > H2;simplify;rewrite > H1;reflexivity
  90   |elim H;rewrite > H2;simplify;rewrite > eqb_n_n;simplify;reflexivity]
  91 qed.*)
  92
  93 axiom swap_other : \forall x,y,z.(z \neq x) \to (z \neq y) \to (swap x y z) = z.
  94 (*intros;unfold swap;elim (eq_eqb_case z x)
  95   [elim H2;lapply (H H3);elim Hletin
  96   |elim H2;rewrite > H4;simplify;elim (eq_eqb_case z y)
  97      [elim H5;lapply (H1 H6);elim Hletin
  98      |elim H5;rewrite > H7;simplify;reflexivity]]
  99 qed.*)
 100
 101 axiom swap_inv : \forall u,v,x.(swap u v (swap u v x)) = x.
 102 (*intros;unfold in match (swap u v x);elim (eq_eqb_case x u)
 103   [elim H;rewrite > H2;simplify;rewrite > H1;apply swap_right
 104   |elim H;rewrite > H2;simplify;elim (eq_eqb_case x v)
 105      [elim H3;rewrite > H5;simplify;rewrite > H4;apply swap_left
 106      |elim H3;rewrite > H5;simplify;apply (swap_other ? ? ? H1 H4)]]
 107 qed.*)
 108
 109 axiom swap_inj : \forall u,v,x,y.(swap u v x) = (swap u v y) \to x = y.
 110 (*intros;unfold swap in H;elim (eq_eqb_case x u)
 111   [elim H1;elim (eq_eqb_case y u)
 112      [elim H4;rewrite > H5;assumption
 113      |elim H4;rewrite > H3 in H;rewrite > H6 in H;simplify in H;
 114       elim (eq_eqb_case y v)
 115         [elim H7;rewrite > H9 in H;simplify in H;rewrite > H in H8;
 116          lapply (H5 H8);elim Hletin
 117         |elim H7;rewrite > H9 in H;simplify in H;elim H8;symmetry;assumption]]
 118   |elim H1;elim (eq_eqb_case y u)
 119      [elim H4;rewrite > H3 in H;rewrite > H6 in H;simplify in H;
 120       elim (eq_eqb_case x v)
 121         [elim H7;rewrite > H9 in H;simplify in H;rewrite < H in H8;
 122          elim H2;assumption
 123         |elim H7;rewrite > H9 in H;simplify in H;elim H8;assumption]
 124      |elim H4;rewrite > H3 in H;rewrite > H6 in H;simplify in H;
 125       elim (eq_eqb_case x v)
 126         [elim H7;rewrite > H9 in H;elim (eq_eqb_case y v)
 127            [elim H10;rewrite > H11;assumption
 128            |elim H10;rewrite > H12 in H;simplify in H;elim H5;symmetry;
 129             assumption]
 130         |elim H7;rewrite > H9 in H;elim (eq_eqb_case y v)
 131            [elim H10;rewrite > H12 in H;simplify in H;elim H2;assumption
 132            |elim H10;rewrite > H12 in H;simplify in H;assumption]]]]
 133 qed.*)
 134
 135 let rec swap_NTyp u v T on T \def
 136   match T with
 137      [(TName X) \Rightarrow (TName (swap u v X))
 138      |NTop \Rightarrow NTop
 139      |(NArrow T1 T2) \Rightarrow (NArrow (swap_NTyp u v T1) (swap_NTyp u v T2))
 140      |(NForall X T1 T2) \Rightarrow
 141                   (NForall (swap u v X) (swap_NTyp u v T1) (swap_NTyp u v T2))].
 142
 143 let rec swap_Typ u v T on T \def
 144   match T with
 145      [(TVar n) \Rightarrow (TVar n)
 146      |(TFree X) \Rightarrow (TFree (swap u v X))
 147      |Top \Rightarrow Top
 148      |(Arrow T1 T2) \Rightarrow (Arrow (swap_Typ u v T1) (swap_Typ u v T2))
 149      |(Forall T1 T2) \Rightarrow (Forall (swap_Typ u v T1) (swap_Typ u v T2))].
 150
 151 definition swap_list : nat \to nat \to (list nat) \to (list nat) ≝
 152   \lambda u,v,l.(map ? ? (swap u v) l).
 153
 154 let rec var_NTyp (T:NTyp):list nat\def
 155   match T with
 156   [TName x ⇒ [x]
 157   |NTop ⇒ []
 158   |NArrow U V ⇒ (var_NTyp U)@(var_NTyp V)
 159   |NForall X U V ⇒ X::(var_NTyp U)@(var_NTyp V)].
 160
 161 inductive alpha_eq : NTyp \to NTyp \to Prop \def
 162 | A_refl : \forall T.(alpha_eq T T)
 163 | A_arrow : \forall T1,T2,U1,U2.(alpha_eq T1 U1) \to (alpha_eq T2 U2) \to
 164                                 (alpha_eq (NArrow T1 T2) (NArrow U1 U2))
 165 | A_forall : \forall T1,T2,U1,U2,X,Y.
 166              (alpha_eq T1 U1) \to
 167              (\forall Z.
 168                  \lnot (in_list nat Z (X::Y::((var_NTyp T2)@(var_NTyp U2))))
 169                  \to (alpha_eq (swap_NTyp Z X T2) (swap_NTyp Z Y U2))) \to
 170              (alpha_eq (NForall X T1 T2) (NForall Y U1 U2)).
 171
 172 let rec posn l x on l \def
 173   match l with
 174   [ nil \Rightarrow O
 175   | (cons (y:nat) l2) \Rightarrow
 176       match (eqb x y) with
 177             [ true \Rightarrow O
 178             | false \Rightarrow S (posn l2 x)]].
 179
 180 let rec length A l on l \def
 181   match l with
 182     [ nil \Rightarrow O
 183     | (cons (y:A) l2) \Rightarrow S (length A l2)].
 184
 185 let rec lookup n l on l \def
 186   match l with
 187     [ nil ⇒ false
 188     | cons (x:nat) l1 \rArr match (eqb n x) with
 189               [true \rArr true
 190               |false \rArr (lookup n l1)]].
 191
 192 let rec encodetype T vars on T \def
 193   match T with
 194   [ (TName n) ⇒ match (lookup n vars) with
 195     [ true ⇒ (TVar (posn vars n))
 196     | false ⇒ (TFree n)]
 197   | NTop ⇒ Top
 198   | (NArrow T1 T2) ⇒ Arrow (encodetype T1 vars) (encodetype T2 vars)
 199   | (NForall n2 T1 T2) ⇒ Forall (encodetype T1 vars)
 200                                 (encodetype T2 (n2::vars))].
 201
 202 let rec head (A:Type) l on l \def
 203   match l with
 204   [ nil \Rightarrow None A
 205   | (cons (x:A) l2) \Rightarrow Some A x].
 206
 207 (*let rec tail (A:Type) l \def
 208   match l with
 209   [ nil \Rightarrow nil A
 210   | (cons (x:A) l2) \Rightarrow l2].*)
 211
 212 let rec nth n l on n \def
 213   match n with
 214   [ O \Rightarrow match l with
 215     [ nil ⇒ O
 216     | (cons x l2) ⇒ x]
 217   | (S n2) \Rightarrow (nth n2 (tail ? l))].
 218
 219 definition max_list : (list nat) \to nat \def
 220   \lambda l.let rec aux l0 m on l0 \def
 221     match l0 with
 222       [ nil ⇒ m
 223       | (cons n l2) ⇒ (aux l2 (max m n))]
 224     in aux l O.
 225
 226 let rec decodetype T vars C on T \def
 227   match T with
 228   [ (TVar n) ⇒ (TName (nth n vars))
 229   | (TFree x)  ⇒ (TName x)
 230   | Top \Rightarrow NTop
 231   | (Arrow T1 T2) ⇒ (NArrow (decodetype T1 vars C) (decodetype T2 vars C))
 232   | (Forall T1 T2) ⇒ (NForall (S (max_list (vars@C))) (decodetype T1 vars C)
 233        (decodetype T2 ((S (max_list (vars@C)))::vars) C))].
 234
 235 definition sublist: \forall A:Type.(list A) \to (list A) \to Prop \def
 236   \lambda A,l1,l2.\forall x.(in_list ? x l1) \to (in_list ? x l2).
 237
 238 let rec remove_nat (x:nat) (l:list nat) on l \def
 239   match l with
 240   [ nil ⇒ (nil nat)
 241   | (cons y l2) ⇒ match (eqb x y) with
 242                   [ true ⇒ (remove_nat x l2)
 243                   | false ⇒ (y :: (remove_nat x l2)) ]].
 244
 245 let rec fv_NTyp (T:NTyp):list nat\def
 246   match T with
 247   [TName x ⇒ [x]
 248   |NTop ⇒ []
 249   |NArrow U V ⇒ (fv_NTyp U)@(fv_NTyp V)
 250   |NForall X U V ⇒ (fv_NTyp U)@(remove_nat X (fv_NTyp V))].
 251
 252
 253 let rec subst_NTyp_var T X Y \def
 254   match T with
 255   [TName Z ⇒ match (eqb X Z) with
 256              [ true \rArr (TName Y)
 257              | false \rArr (TName Z) ]
 258   |NTop ⇒ NTop
 259   |NArrow U V ⇒ (NArrow (subst_NTyp_var U X Y) (subst_NTyp_var V X Y))
 260   |NForall Z U V ⇒ match (eqb X Z) with
 261                    [ true ⇒ (NForall Z (subst_NTyp_var U X Y) V)
 262                    | false ⇒ (NForall Z (subst_NTyp_var U X Y)
 263                                         (subst_NTyp_var V X Y))]].
 264
 265 definition fv_Nenv : list nbound → list nat ≝
 266   map nbound nat
 267     (λb.match b with
 268       [mk_nbound (B:bool) (X:nat) (T:NTyp) ⇒ X]).
 269
 270 inductive NWFType : (list nbound) → NTyp → Prop ≝
 271   | NWFT_TName : ∀X,G.(in_list ? X (fv_Nenv G))
 272                 → (NWFType G (TName X))
 273   | NWFT_Top : ∀G.(NWFType G NTop)
 274   | NWFT_Arrow : ∀G,T,U.(NWFType G T) → (NWFType G U) →
 275                 (NWFType G (NArrow T U))
 276   | NWFT_Forall : ∀G,X,T,U.(NWFType G T) →
 277                   (∀Y.¬(Y ∈ (fv_Nenv G)) →
 278                        (Y = X ∨ ¬(Y ∈ (fv_NTyp U))) →
 279                     (NWFType ((mk_nbound true Y T) :: G) (swap_NTyp Y X U))) →
 280                  (NWFType G (NForall X T U)).
 281   (*NWFT_alpha : ∀G,T,U.(NWFType G T) → (alpha_eq T U) → (NWFType G U).*)
 282
 283 inductive NWFEnv : (list nbound) → Prop ≝
 284   | NWFE_Empty : (NWFEnv (nil ?))
 285   | NWFE_cons : ∀B,X,T,G.(NWFEnv G) →
 286                   ¬(in_list ? X (fv_Nenv G)) →
 287                   (NWFType G T) → (NWFEnv ((mk_nbound B X T) :: G)).
 288
 289 inductive NJSubtype : (list nbound) → NTyp → NTyp → Prop ≝
 290   | NSA_Top : ∀G,T.(NWFEnv G) → (NWFType G T) → (NJSubtype G T NTop)
 291   | NSA_Refl_TVar : ∀G,X.(NWFEnv G)
 292                    → (in_list ? X (fv_Nenv G))
 293                    → (NJSubtype G (TName X) (TName X))
 294   | NSA_Trans_TVar : ∀G,X,T,U.
 295                      (in_list ? (mk_nbound true X U) G) →
 296                      (NJSubtype G U T) → (NJSubtype G (TName X) T)
 297   | NSA_Arrow : ∀G,S1,S2,T1,T2.
 298                (NJSubtype G T1 S1) → (NJSubtype G S2 T2) →
 299                (NJSubtype G (NArrow S1 S2) (NArrow T1 T2))
 300   | NSA_All : ∀G,X,Y,S1,S2,T1,T2.
 301               (NWFType G (NForall X S1 S2)) \to
 302               (NWFType G (NForall Y T1 T2)) \to
 303               (NJSubtype G T1 S1) →
 304               (∀Z.¬(Z ∈ fv_Nenv G) →
 305                   (Z = X \lor \lnot in_list ? Z (fv_NTyp S2)) \to
 306                   (Z = Y \lor \lnot in_list ? Z (fv_NTyp T2)) \to
 307               (NJSubtype ((mk_nbound true Z T1) :: G)
 308                     (swap_NTyp Z X S2) (swap_NTyp Z Y T2))) →
 309               (NJSubtype G (NForall X S1 S2) (NForall Y T1 T2))
 310   | NSA_alpha : ∀G,T1,T2,U1,U2.(NJSubtype G T1 U1) →
 311                                 (alpha_eq T1 T2) →
 312                                 (alpha_eq U1 U2) →
 313                                 (NJSubtype G T2 U2).
 314
 315 let rec nt_len T \def
 316   match T with
 317   [ TName X ⇒ O
 318   | NTop ⇒ O
 319   | NArrow T1 T2 ⇒ S (max (nt_len T1) (nt_len T2))
 320   | NForall X T1 T2 ⇒ S (max (nt_len T1) (nt_len T2)) ].
 321
 322 definition encodeenv : list nbound → list bound ≝
 323   map nbound bound
 324     (λb.match b with
 325        [ mk_nbound b x T ⇒ mk_bound b x (encodetype T []) ]).
 326
 327 axiom append_associative : ∀A.∀l1,l2,l3:(list A).((l1@l2)@l3) = (l1@l2@l3).
 328
 329 lemma eq_fv_Nenv_fv_env : ∀G. fv_Nenv G = fv_env (encodeenv G).
 330 intro;elim G
 331   [simplify;reflexivity
 332   |simplify;rewrite < H;elim t;simplify;reflexivity]
 333 qed.
 334
 335 (* palloso *)
 336 axiom decidable_eq_bound : \forall b,c:bound.decidable (b = c).
 337
 338 lemma in_Nenv_to_in_env: ∀l,n,n2.mk_nbound true n n2 ∈ l →
 339                  mk_bound true n (encodetype n2 []) ∈ encodeenv l.
 340 intros 3;elim l
 341   [elim (not_in_list_nil ? ? H)
 342   |inversion H1;intros
 343      [destruct;simplify;apply in_list_head
 344      |destruct;elim t;simplify;apply in_list_cons;apply H;assumption]]
 345 qed.
 346
 347 lemma in_lookup : \forall x,l.(in_list ? x l) \to (lookup x l = true).
 348 intros;elim H
 349   [simplify;rewrite > eqb_n_n;reflexivity
 350   |simplify;rewrite > H2;elim (eqb a a1);reflexivity]
 351 qed.
 352
 353 lemma lookup_in : \forall x,l.(lookup x l = true) \to (in_list ? x l).
 354 intros 2;elim l
 355   [simplify in H;destruct H
 356   |generalize in match H1;simplify;elim (decidable_eq_nat x t)
 357      [rewrite > H2;apply in_list_head
 358      |rewrite > (not_eq_to_eqb_false ? ? H2) in H3;simplify in H3;
 359       apply in_list_cons;apply H;assumption]]
 360 qed.
 361
 362 lemma posn_length : \forall x,vars.(in_list ? x vars) \to
 363                        (posn vars x) < (length ? vars).
 364 intros 2;elim vars
 365   [elim (not_in_list_nil ? ? H)
 366   |inversion H1
 367      [intros;destruct;simplify;rewrite > eqb_n_n;simplify;
 368       apply lt_O_S
 369      |intros;destruct;simplify;elim (eqb x t);simplify
 370         [apply lt_O_S
 371         |apply le_S_S;apply H;assumption]]]
 372 qed.
 373
 374 lemma in_remove : \forall a,b,l.(a \neq b) \to (in_list ? a l) \to
 375                                 (in_list ? a (remove_nat b l)).
 376 intros 4;elim l
 377   [elim (not_in_list_nil ? ? H1)
 378   |inversion H2;intros;
 379      [destruct;simplify;rewrite > not_eq_to_eqb_false
 380         [simplify;apply in_list_head
 381         |intro;apply H;symmetry;assumption]
 382      |destruct;simplify;elim (eqb b t)
 383         [simplify;apply H1;assumption
 384         |simplify;apply in_list_cons;apply H1;assumption]]]
 385 qed.
 386
 387 axiom NTyp_len_ind : \forall P:NTyp \to Prop.
 388                        (\forall U.(\forall V.((nt_len V) < (nt_len U)) \to (P V))
 389                            \to (P U))
 390                        \to \forall T.(P T).
 391
 392 axiom ntlen_arrow1 : ∀T1,T2.(nt_len T1) < (nt_len (NArrow T1 T2)).
 393 axiom ntlen_arrow2 : ∀T1,T2.(nt_len T2) < (nt_len (NArrow T1 T2)).
 394 axiom ntlen_forall1 : ∀X,T1,T2.(nt_len T1) < (nt_len (NForall X T1 T2)).
 395 axiom ntlen_forall2 : ∀X,T1,T2.(nt_len T2) < (nt_len (NForall X T1 T2)).
 396 axiom eq_ntlen_swap : ∀X,Y,T.nt_len T = nt_len (swap_NTyp X Y T).
 397
 398 axiom nat_in_list_case :\forall G:list nat
 399 .\forall H:list nat
 400  .\forall n:nat.in_list nat n (H@G)\rarr in_list nat n G\lor in_list nat n H.
 401
 402 lemma swap_same : \forall x,y.swap x x y = y.
 403 intros;elim (decidable_eq_nat y x)
 404   [autobatch paramodulation
 405   |rewrite > swap_other;autobatch]
 406 qed.
 407
 408 lemma not_nat_in_to_lookup_false : ∀l,X.¬(X ∈ l) → lookup X l = false.
 409 intros 2;elim l
 410   [simplify;reflexivity
 411   |simplify;elim (decidable_eq_nat X t)
 412      [elim H1;rewrite > H2;apply in_list_head
 413      |rewrite > (not_eq_to_eqb_false ? ? H2);simplify;apply H;intro;apply H1;
 414       apply (in_list_cons ? ? ? ? H3);]]
 415 qed.
 416
 417 lemma fv_encode : ∀T,l1,l2.
 418                   (∀x.(in_list ? x (fv_NTyp T)) →
 419                      (lookup x l1 = lookup x l2 ∧
 420                      (lookup x l1 = true → posn l1 x = posn l2 x))) →
 421                   (encodetype T l1 = encodetype T l2).
 422 intro;elim T
 423   [simplify in H;elim (H n)
 424      [simplify;rewrite < H1;generalize in match H2;elim (lookup n l1)
 425         [simplify;rewrite > H3;autobatch
 426         |simplify;reflexivity]
 427      |apply in_list_head]
 428   |simplify;reflexivity
 429   |simplify;rewrite > (H l1 l2)
 430      [rewrite > (H1 l1 l2)
 431         [reflexivity
 432         |intros;apply H2;simplify;apply in_list_to_in_list_append_r;autobatch]
 433      |intros;apply H2;simplify;apply in_list_to_in_list_append_l;autobatch]
 434   |simplify;rewrite > (H l1 l2)
 435      [rewrite > (H1 (n::l1) (n::l2))
 436         [reflexivity
 437         |intros;elim (decidable_eq_nat x n)
 438            [simplify;rewrite > (eq_to_eqb_true ? ? H4);simplify;split
 439               [reflexivity|intro;reflexivity]
 440            |elim (H2 x)
 441               [split
 442                  [simplify;rewrite < H5;reflexivity
 443                  |simplify;elim (eqb x n);
 444                     [simplify;reflexivity
 445                     |simplify in H7;rewrite < (H6 H7);reflexivity]]
 446               |simplify;apply in_list_to_in_list_append_r;
 447                apply (in_remove ? ? ? H4);assumption]]]
 448      |intros;apply H2;simplify;apply in_list_to_in_list_append_l;autobatch]]
 449 qed.
 450
 451 lemma lookup_swap : \forall a,b,x,vars.
 452                     (lookup (swap a b x) (swap_list a b vars) =
 453                     lookup x vars).
 454 intros 4;elim vars
 455   [simplify;reflexivity
 456   |simplify;elim (decidable_eq_nat x t)
 457      [rewrite > H1;rewrite > eqb_n_n;rewrite > eqb_n_n;simplify;reflexivity
 458      |rewrite > (not_eq_to_eqb_false ? ? H1);elim (decidable_eq_nat x a)
 459         [rewrite > H;rewrite > H2;rewrite > swap_left;
 460          elim (decidable_eq_nat b t)
 461            [rewrite < H3;rewrite > swap_right;
 462             rewrite > (not_eq_to_eqb_false b a)
 463               [reflexivity
 464               |intro;autobatch]
 465            |rewrite > (swap_other a b t)
 466               [rewrite > (not_eq_to_eqb_false ? ? H3);simplify;reflexivity
 467               |intro;autobatch
 468               |intro;autobatch]]
 469         |elim (decidable_eq_nat x b)
 470            [rewrite > H;rewrite > H3;rewrite > swap_right;
 471             elim (decidable_eq_nat t a)
 472               [rewrite > H4;rewrite > swap_left;
 473                rewrite > (not_eq_to_eqb_false a b)
 474                  [reflexivity
 475                  |intro;autobatch]
 476               |rewrite > (swap_other a b t)
 477                  [rewrite > (not_eq_to_eqb_false a t)
 478                     [reflexivity
 479                     |intro;autobatch]
 480                  |assumption
 481                  |intro;autobatch]]
 482            |rewrite > H;rewrite > (swap_other a b x)
 483               [elim (decidable_eq_nat a t)
 484                  [rewrite > H4;rewrite > swap_left;
 485                   rewrite > (not_eq_to_eqb_false ? ? H3);reflexivity
 486                  |elim (decidable_eq_nat b t)
 487                     [rewrite > H5;rewrite > swap_right;
 488                      rewrite > (not_eq_to_eqb_false ? ? H2);reflexivity
 489                     |rewrite > (swap_other a b t)
 490                        [rewrite > (not_eq_to_eqb_false ? ? H1);reflexivity
 491                        |intro;autobatch
 492                        |intro;autobatch]]]
 493               |assumption
 494               |assumption]]]]]
 495 qed.
 496
 497 lemma posn_swap : \forall a,b,x,vars.
 498                   (posn vars x = posn (swap_list a b vars) (swap a b x)).
 499 intros 4;elim vars
 500   [simplify;reflexivity
 501   |simplify;rewrite < H;elim (decidable_eq_nat x t)
 502      [rewrite > H1;do 2 rewrite > eqb_n_n;reflexivity
 503      |elim (decidable_eq_nat (swap a b x) (swap a b t))
 504         [elim H1;autobatch
 505         |rewrite > (not_eq_to_eqb_false ? ? H1);
 506          rewrite > (not_eq_to_eqb_false ? ? H2);reflexivity]]]
 507 qed.
 508
 509 theorem encode_swap : ∀a,x,T,vars.
 510                          ((in_list ? a (fv_NTyp T)) → (in_list ? a vars)) →
 511                          (in_list ? x vars) →
 512                       encodetype T vars =
 513                       encodetype (swap_NTyp a x T) (swap_list a x vars).
 514 intros 3;elim T
 515   [elim (decidable_eq_nat n x)
 516      [rewrite > H2;simplify in match (swap_NTyp ? ? ?);rewrite > swap_right;
 517       simplify;lapply (lookup_swap a x x vars);rewrite > swap_right in Hletin;
 518       rewrite > Hletin;cut ((in_list ? x vars) \to (lookup x vars = true))
 519         [rewrite > (Hcut H1);simplify;lapply (posn_swap a x x vars);
 520          rewrite > swap_right in Hletin1;rewrite < Hletin1;reflexivity
 521         |generalize in match x;elim vars
 522            [elim (not_in_list_nil ? ? H3)
 523            |inversion H4
 524               [intros;simplify;rewrite > eqb_n_n;reflexivity
 525               |intros;simplify;destruct;rewrite > (H3 ? H5);
 526                elim (eqb n1 t);reflexivity]]]
 527      |elim (decidable_eq_nat n a);
 528         [rewrite < H3;simplify;rewrite < posn_swap;rewrite > lookup_swap;
 529          rewrite < H3 in H;simplify in H;rewrite > in_lookup;
 530            [simplify;reflexivity
 531            |apply H;apply in_list_head]
 532         |simplify in ⊢ (? ? ? (? % ?));rewrite > swap_other;
 533            [apply (fv_encode ? vars (swap_list a x vars));intros;
 534             simplify in H4;cut (x1 = n)
 535               [rewrite > Hcut;elim vars
 536                  [simplify;split [reflexivity|intro;reflexivity]
 537                  |simplify;elim H5;cut
 538                     (t = a ∨t = x ∨ (t ≠ a ∧ t ≠ x))
 539                     [|elim (decidable_eq_nat t a)
 540                        [left;left;assumption
 541                        |elim (decidable_eq_nat t x)
 542                           [left;right;assumption
 543                           |right;split;assumption]]]
 544                   elim Hcut1
 545                     [elim H8
 546                        [rewrite > H9;rewrite > swap_left;
 547                         rewrite > (not_eq_to_eqb_false ? ? H2);
 548                         rewrite > (not_eq_to_eqb_false ? ? H3);simplify;
 549                         split
 550                           [assumption
 551                           |intro;rewrite < (H7 H10);reflexivity]
 552                        |rewrite > H9;rewrite > swap_right;
 553                         rewrite > (not_eq_to_eqb_false ? ? H2);
 554                         rewrite > (not_eq_to_eqb_false ? ? H3);simplify;
 555                         split
 556                           [assumption
 557                           |intro;rewrite < (H7 H10);reflexivity]]
 558                     |elim H8;rewrite > (swap_other a x t)
 559                        [rewrite < H6;split
 560                           [reflexivity
 561                           |elim (eqb n t)
 562                              [simplify;reflexivity
 563                              |simplify in H11;rewrite < (H7 H11);reflexivity]]
 564                        |*:assumption]]]
 565               |inversion H4
 566                  [intros;destruct;reflexivity
 567                  |intros;destruct;elim (not_in_list_nil ? ? H5)]]
 568            |*:assumption]]]
 569   |simplify;reflexivity
 570   |simplify;simplify in H2;rewrite < H
 571      [rewrite < H1
 572         [reflexivity
 573         |intro;apply H2;apply in_list_to_in_list_append_r;autobatch
 574         |assumption]
 575      |intro;apply H2;apply in_list_to_in_list_append_l;autobatch
 576      |assumption]
 577   |simplify;simplify in H2;rewrite < H
 578      [elim (decidable_eq_nat a n)
 579         [rewrite < (H1 (n::vars));
 580            [reflexivity
 581            |intro;rewrite > H4;apply in_list_head
 582            |apply in_list_cons;assumption]
 583         |rewrite < (H1 (n::vars));
 584            [reflexivity
 585            |intro;apply in_list_cons;apply H2;apply in_list_to_in_list_append_r;
 586             apply (in_remove ? ? ? H4 H5)
 587            |apply in_list_cons;assumption]]
 588      |intro;apply H2;apply in_list_to_in_list_append_l;assumption
 589      |assumption]]
 590 qed.
 591
 592 lemma encode_swap2 : ∀a:nat.∀x:nat.∀T:NTyp.
 593   ¬(a ∈ (fv_NTyp T)) →
 594     \forall vars.x ∈ vars
 595        →encodetype T vars=encodetype (swap_NTyp a x T) (swap_list a x vars).
 596 intros;apply (encode_swap ? ? ? ? ? H1);intro;elim (H H2);
 597 qed.
 598
 599 lemma remove_inlist : \forall x,y,l.(in_list ? x (remove_nat y l)) \to
 600                       (in_list ? x l) \land x \neq y.
 601 intros 3;elim l 0
 602   [simplify;intro;elim (not_in_list_nil ? ? H)
 603   |simplify;intro;elim (decidable_eq_nat y t)
 604      [rewrite > H in H2;rewrite > eqb_n_n in H2;simplify in H2;
 605       rewrite > H in H1;elim (H1 H2);rewrite > H;split
 606         [apply in_list_cons;assumption
 607         |assumption]
 608      |rewrite > (not_eq_to_eqb_false ? ? H) in H2;simplify in H2;
 609       inversion H2
 610         [intros;destruct;split
 611            [apply in_list_head
 612            |intro;autobatch]
 613         |intros;destruct;
 614          elim (H1 H3);split
 615            [apply in_list_cons;assumption
 616            |assumption]]]]
 617 qed.
 618
 619 lemma inlist_remove : \forall x,y,l.(in_list ? x l \to x \neq y \to
 620                 (in_list ? x (remove_nat y l))).
 621 intros 3;elim l
 622   [elim (not_in_list_nil ? ? H);
 623   |simplify;elim (decidable_eq_nat y t)
 624      [rewrite > (eq_to_eqb_true ? ? H3);simplify;apply H
 625         [(*FIXME*)generalize in match H1;intro;inversion H1
 626            [intros;destruct;elim H2;reflexivity
 627            |intros;destruct;assumption]
 628         |assumption]
 629      |rewrite > (not_eq_to_eqb_false ? ? H3);simplify;
 630       (*FIXME*)generalize in match H1;intro;inversion H4
 631         [intros;destruct;apply in_list_head
 632         |intros;destruct;apply in_list_cons;apply (H H5 H2)
 633         ]]]
 634 qed.
 635
 636 lemma incl_fv_var : \forall T.(incl ? (fv_NTyp T) (var_NTyp T)).
 637 intro;elim T
 638   [simplify;unfold;intros;assumption
 639   |simplify;unfold;intros;assumption
 640   |simplify;unfold;intros;elim (in_list_append_to_or_in_list ? ? ? ? H2)
 641      [apply in_list_to_in_list_append_l;apply (H ? H3)
 642      |apply in_list_to_in_list_append_r;apply (H1 ? H3)]
 643   |simplify;unfold;intros;elim (decidable_eq_nat x n)
 644      [rewrite > H3;apply in_list_head
 645      |apply in_list_cons;elim (in_list_append_to_or_in_list ? ? ? ? H2)
 646         [apply in_list_to_in_list_append_l;apply (H ? H4)
 647         |apply in_list_to_in_list_append_r;elim (remove_inlist ? ? ? H4);
 648          apply (H1 ? H5)]]]
 649 qed.
 650
 651 lemma fv_encode2 : ∀T,l1,l2.
 652                       (∀x.(in_list ? x (fv_NTyp T)) →
 653                            (lookup x l1 = lookup x l2 ∧
 654                             posn l1 x = posn l2 x)) →
 655                       (encodetype T l1 = encodetype T l2).
 656 intros;apply fv_encode;intros;elim (H ? H1);split
 657   [assumption|intro;assumption]
 658 qed.
 659
 660 lemma alpha_sym : \forall S,T.(alpha_eq S T) \to (alpha_eq T S).
 661 intros;elim H
 662   [apply A_refl
 663   |apply A_arrow;assumption
 664   |apply A_forall
 665      [assumption
 666      |intros;apply H4;intro;apply H5;elim (decidable_eq_nat Z n5)
 667         [rewrite > H7;apply in_list_head
 668         |apply in_list_cons;(*FIXME*)generalize in match H6;intro;
 669          inversion H6
 670            [intros;destruct;apply in_list_head
 671            |intros;destruct;apply in_list_cons;inversion H9
 672               [intros;destruct;elim H7;reflexivity
 673               |intros;destruct;
 674                elim (in_list_append_to_or_in_list ? ? ? ? H11)
 675                  [apply in_list_to_in_list_append_r;assumption
 676                  |apply in_list_to_in_list_append_l;assumption]]]]]]
 677 qed.
 678
 679 lemma inlist_fv_swap : \forall x,y,b,T.
 680                    (\lnot (in_list ? b (y::var_NTyp T))) \to
 681                    (in_list ? x (fv_NTyp (swap_NTyp b y T))) \to
 682                    (x \neq y \land (x = b \lor (in_list ? x (fv_NTyp T)))).
 683 intros 4;elim T
 684   [simplify in H;simplify;simplify in H1;elim (decidable_eq_nat y n)
 685      [rewrite > H2 in H1;rewrite > swap_right in H1;
 686       inversion H1
 687         [intros;destruct;split
 688            [unfold;intro;apply H;rewrite > H2;apply in_list_head
 689            |left;reflexivity]
 690         |intros;destruct;elim (not_in_list_nil ? ? H3)]
 691      |elim (decidable_eq_nat b n)
 692         [rewrite > H3 in H;elim H;apply in_list_cons;apply in_list_head
 693         |rewrite > swap_other in H1
 694            [split
 695               [inversion H1
 696                  [intros;destruct;intro;apply H2;
 697                   symmetry;assumption
 698                  |intros;destruct;
 699                   elim (not_in_list_nil ? ? H4)]
 700               |autobatch]
 701            |intro;autobatch
 702            |intro;autobatch]]]
 703   |simplify in H1;elim (not_in_list_nil ? ? H1)
 704   |simplify;simplify in H3;simplify in H2;elim (nat_in_list_case ? ? ? H3)
 705      [elim H1
 706         [split
 707            [assumption
 708            |elim H6
 709               [left;assumption
 710               |right;apply in_list_to_in_list_append_r;assumption]]
 711            |intro;apply H2;elim (nat_in_list_case (var_NTyp n1) [y] ? H5)
 712               [apply (in_list_to_in_list_append_r ? ? (y::var_NTyp n) (var_NTyp n1));
 713                assumption
 714               |inversion H6
 715                  [intros;destruct;apply in_list_head
 716                  |intros;destruct;
 717                   elim (not_in_list_nil ? ? H7)]]
 718            |assumption]
 719         |elim H
 720            [split
 721               [assumption
 722               |elim H6
 723                  [left;assumption
 724                  |right;apply in_list_to_in_list_append_l;assumption]]
 725            |intro;apply H2;inversion H5
 726               [intros;destruct;apply in_list_head
 727               |intros;destruct;apply in_list_cons;
 728                apply in_list_to_in_list_append_l;assumption]
 729            |assumption]]
 730    |simplify;simplify in H3;simplify in H2;elim (nat_in_list_case ? ? ? H3)
 731       [elim H1
 732          [split
 733             [assumption
 734             |elim H6
 735                [left;assumption
 736                |right;apply in_list_to_in_list_append_r;apply inlist_remove
 737                   [assumption
 738                   |intro;elim (remove_inlist ? ? ? H4);apply H10;
 739                    rewrite > swap_other
 740                      [assumption
 741                      |intro;rewrite > H8 in H7;rewrite > H11 in H7;apply H2;
 742                       destruct;apply in_list_cons;apply in_list_head
 743                      |destruct;assumption]]]]
 744          |intro;apply H2;inversion H5
 745             [intros;destruct;apply in_list_head
 746             |intros;destruct;
 747              apply in_list_cons;
 748              cut ((n::var_NTyp n1)@(var_NTyp n2) = n::var_NTyp n1@var_NTyp n2)
 749                [rewrite < Hcut;elim (n::var_NTyp n1)
 750                   [simplify;assumption
 751                   |simplify;elim (decidable_eq_nat b t)
 752                      [rewrite > H9;apply in_list_head
 753                      |apply in_list_cons;assumption]]
 754                |simplify;reflexivity]]
 755          |elim(remove_inlist ? ? ? H4);assumption]
 756       |elim H
 757          [split
 758             [assumption
 759             |elim H6
 760                [left;assumption
 761                   |right;apply in_list_to_in_list_append_l;
 762                    assumption]]
 763             |intro;apply H2;inversion H5
 764                [intros;destruct;apply in_list_head
 765                |intros;destruct;apply in_list_cons;
 766                 elim (decidable_eq_nat b n)
 767                   [rewrite > H8;apply in_list_head
 768                   |apply in_list_cons;apply in_list_to_in_list_append_l;
 769                    assumption]]
 770             |assumption]]]
 771 qed.
 772
 773 lemma inlist_fv_swap_r : \forall x,y,b,T.
 774                    (\lnot (in_list ? b (y::var_NTyp T))) \to
 775                    ((x = b \land (in_list ? y (fv_NTyp T))) \lor
 776                     (x \neq y \land (in_list ? x (fv_NTyp T)))) \to
 777                    (in_list ? x (fv_NTyp (swap_NTyp b y T))).
 778 intros 4;elim T
 779   [simplify;simplify in H;simplify in H1;cut (b \neq n)
 780      [elim H1
 781         [elim H2;cut (y = n)
 782            [rewrite > Hcut1;rewrite > swap_right;rewrite > H3;apply in_list_head
 783            |inversion H4
 784               [intros;destruct;autobatch
 785               |intros;destruct;elim (not_in_list_nil ? ? H5)]]
 786         |elim H2;inversion H4
 787            [intros;destruct;rewrite > (swap_other b y x)
 788               [apply in_list_head
 789               |intro;autobatch
 790               |assumption]
 791            |intros;destruct;elim (not_in_list_nil ? ? H5)]]
 792         |intro;apply H;apply (in_list_to_in_list_append_r ? ? [y] [n]);
 793          rewrite > H2;apply in_list_head]
 794   |simplify in H1;elim H1;elim H2;elim (not_in_list_nil ? ? H4)
 795   |simplify;simplify in H3;cut (\lnot (in_list ? b (y::var_NTyp n1)))
 796      [cut (\lnot (in_list ? b (y::var_NTyp n)))
 797         [elim H3
 798            [elim H4;elim (in_list_append_to_or_in_list ? ? ? ? H6)
 799               [apply in_list_to_in_list_append_l;apply H
 800                  [assumption
 801                  |left;split;assumption]
 802               |apply in_list_to_in_list_append_r;apply H1
 803                  [assumption
 804                  |left;split;assumption]]
 805            |elim H4;elim (in_list_append_to_or_in_list ? ? ? ? H6)
 806               [apply in_list_to_in_list_append_l;apply H;
 807                  [assumption
 808                  |right;split;assumption]
 809               |apply in_list_to_in_list_append_r;apply H1
 810                  [assumption
 811                  |right;split;assumption]]]
 812         |intro;apply H2;inversion H4
 813            [intros;destruct;apply in_list_head
 814            |intros;destruct;apply in_list_cons;
 815             simplify;apply in_list_to_in_list_append_l;
 816             assumption]]
 817      |intro;apply H2;inversion H4
 818         [intros;destruct;apply in_list_head
 819         |intros;destruct;apply in_list_cons;
 820          simplify;apply in_list_to_in_list_append_r;
 821          assumption]]
 822   |simplify;simplify in H3;cut (\lnot (in_list ? b (y::var_NTyp n1)))
 823      [cut (\lnot (in_list ? b (y::var_NTyp n2)))
 824         [elim H3
 825            [elim H4;elim (in_list_append_to_or_in_list ? ? ? ? H6)
 826               [apply in_list_to_in_list_append_l;apply H
 827                  [assumption
 828                  |left;split;assumption]
 829               |apply in_list_to_in_list_append_r;apply inlist_remove
 830                  [apply H1;
 831                     [assumption
 832                     |left;split
 833                        [assumption|elim (remove_inlist ? ? ? H7);assumption]]
 834                  |elim (remove_inlist ? ? ? H7);elim (decidable_eq_nat b n)
 835                     [rewrite > H10;rewrite > swap_left;intro;apply H9;
 836                      rewrite < H11;rewrite < H10;assumption
 837                     |rewrite > swap_other
 838                        [rewrite > H5;assumption
 839                        |intro;apply H10;symmetry;assumption
 840                        |intro;apply H9;symmetry;assumption]]]]
 841            |elim H4;elim (in_list_append_to_or_in_list ? ? ? ? H6)
 842               [apply in_list_to_in_list_append_l;apply H
 843                  [assumption
 844                  |right;split;assumption]
 845               |apply in_list_to_in_list_append_r;apply inlist_remove
 846                  [apply H1;
 847                     [assumption
 848                     |right;split
 849                        [assumption|elim (remove_inlist ? ? ? H7);assumption]]
 850                  |elim (decidable_eq_nat b n)
 851                     [rewrite > H8;rewrite > swap_left;assumption
 852                     |elim (decidable_eq_nat y n)
 853                        [rewrite > H9;rewrite > swap_right;intro;apply Hcut1;
 854                         rewrite > H9;apply in_list_cons;
 855                         apply incl_fv_var;elim (remove_inlist ? ? ? H7);
 856                         rewrite < H10;assumption
 857                        |rewrite > (swap_other b y n)
 858                           [elim (remove_inlist ? ? ? H7);assumption
 859                           |intro;autobatch
 860                           |intro;autobatch]]]]]]
 861         |intro;apply H2;inversion H4
 862            [intros;destruct;apply in_list_head
 863            |simplify;intros;destruct;
 864             apply in_list_cons;
 865             apply (in_list_to_in_list_append_r ? ? (n::var_NTyp n1) (var_NTyp n2));
 866             assumption]]
 867      |intro;apply H2;inversion H4
 868         [intros;destruct;apply in_list_head
 869         |simplify;intros;destruct;
 870          apply in_list_cons;
 871          apply (in_list_to_in_list_append_l ? ? (n::var_NTyp n1) (var_NTyp n2));
 872          apply in_list_cons;assumption]]]
 873 qed.
 874
 875 lemma fv_alpha : \forall S,T.(alpha_eq S T) \to
 876                  (incl ? (fv_NTyp S) (fv_NTyp T)).
 877 intros;elim H
 878   [unfold;intros;assumption
 879   |simplify;unfold;intros;elim (in_list_append_to_or_in_list ? ? ? ? H5)
 880      [apply in_list_to_in_list_append_l;autobatch
 881      |apply in_list_to_in_list_append_r;autobatch]
 882   |simplify;unfold;intros;
 883    elim (in_list_append_to_or_in_list ? ? ? ? H5)
 884      [apply in_list_to_in_list_append_l;apply (H2 ? H6)
 885      |elim (fresh_name (n4::n5::var_NTyp n1@var_NTyp n3));
 886       apply in_list_to_in_list_append_r;
 887       lapply (H4 ? H7);
 888       elim (remove_inlist ? ? ? H6);apply inlist_remove
 889         [lapply (inlist_fv_swap_r x n4 a n1)
 890            [elim (inlist_fv_swap x n5 a n3)
 891               [elim H11
 892                  [rewrite < H12 in H7;elim H7;
 893                   do 2 apply in_list_cons;
 894                   apply in_list_to_in_list_append_l;
 895                   apply (incl_fv_var n1 ? H8);
 896                  |assumption]
 897               |intro;apply H7;inversion H10;intros;destruct;
 898                  [apply in_list_cons;apply in_list_head
 899                  |do 2 apply in_list_cons;apply in_list_to_in_list_append_r;
 900                   assumption]
 901               |apply (Hletin ? Hletin1)]
 902            |intro;apply H7;inversion H10
 903               [intros;destruct;apply in_list_head
 904               |intros;destruct;do 2 apply in_list_cons;
 905                apply in_list_to_in_list_append_l;assumption]
 906            |right;split;assumption]
 907         |intros;intro;lapply (inlist_fv_swap_r x n4 a n1)
 908            [lapply (Hletin ? Hletin1);
 909             elim (inlist_fv_swap x n5 a n3 ? Hletin2)
 910               [apply (H11 H10)
 911               |intro;apply H7;elim (decidable_eq_nat a n4)
 912                  [rewrite > H12;apply in_list_head
 913                  |apply in_list_cons;inversion H11;intros;destruct;
 914                     [apply in_list_head
 915                     |apply in_list_cons;apply in_list_to_in_list_append_r;
 916                      assumption]]]
 917            |intro;apply H7;inversion H11
 918               [intros;destruct;apply in_list_head
 919               |intros;destruct;do 2 apply in_list_cons;
 920                apply in_list_to_in_list_append_l;assumption]
 921            |right;split;assumption]]]]
 922 qed.
 923
 924 theorem alpha_to_encode : ∀S,T.(alpha_eq S T) →
 925                              ∀vars.(encodetype S vars) = (encodetype T vars).
 926 intros 3;elim H
 927   [reflexivity
 928   |simplify;rewrite > H2;rewrite > H4;reflexivity
 929   |simplify;rewrite > H2;
 930    cut (encodetype n1 (n4::vars) = encodetype n3 (n5::vars))
 931      [rewrite > Hcut;reflexivity
 932      |elim (fresh_name (n4::n5::var_NTyp n1@var_NTyp n3));
 933       lapply (encode_swap2 a n4 n1 ? (n4::vars))
 934         [intro;apply H5;do 2 apply in_list_cons;
 935          apply in_list_to_in_list_append_l;autobatch
 936         |lapply (encode_swap2 a n5 n3 ? (n5::vars))
 937            [intro;apply H5;do 2 apply in_list_cons;
 938             apply in_list_to_in_list_append_r;autobatch
 939            |rewrite > Hletin;rewrite > Hletin1;simplify;rewrite > swap_right;
 940             rewrite > swap_right;rewrite > (H4 a H5 (a::swap_list a n4 vars));
 941             rewrite > (fv_encode2 ? ? (a::swap_list a n5 vars))
 942               [reflexivity
 943               |intros;elim (decidable_eq_nat n4 n5)
 944                  [rewrite > H7;autobatch
 945                  |cut ((x \neq n4) \land (x \neq n5))
 946                     [elim Hcut;elim (decidable_eq_nat x a)
 947                        [simplify;rewrite > (eq_to_eqb_true ? ? H10);simplify;
 948                         autobatch
 949                        |simplify;rewrite > (not_eq_to_eqb_false ? ? H10);
 950                         simplify;elim vars
 951                              [simplify;autobatch
 952                              |simplify;elim H11;rewrite < H12;
 953                               rewrite > H13;elim (decidable_eq_nat a t)
 954                                 [rewrite > H14;rewrite > swap_left;
 955                                  rewrite > swap_left;
 956                                  rewrite > (not_eq_to_eqb_false ? ? H8);
 957                                  rewrite > (not_eq_to_eqb_false ? ? H9);
 958                                  simplify;autobatch
 959                                 |elim (decidable_eq_nat n4 t)
 960                                    [rewrite > H15;rewrite > swap_right;
 961                                     rewrite > (swap_other a n5 t)
 962                                        [rewrite > (not_eq_to_eqb_false ? ? H10);
 963                                         rewrite < H15;
 964                                         rewrite > (not_eq_to_eqb_false ? ? H8);
 965                                         autobatch
 966                                        |intro;autobatch
 967                                        |intro;apply H7;autobatch]
 968                                    |rewrite > (swap_other a n4 t);
 969                                     elim (decidable_eq_nat n5 t)
 970                                       [rewrite < H16;rewrite > swap_right;
 971                                     rewrite > (not_eq_to_eqb_false ? ? H9);
 972                                     rewrite > (not_eq_to_eqb_false ? ? H10);
 973                                     autobatch
 974                                    |rewrite > (swap_other a n5 t);try intro;
 975                                     autobatch
 976                                    |*:intro;autobatch]]]]]
 977                        |split
 978                           [lapply (H3 ? H5);lapply (alpha_sym ? ? Hletin2);
 979                            lapply (fv_alpha ? ? Hletin3);
 980                            lapply (Hletin4 ? H6);
 981                            elim (inlist_fv_swap ? ? ? ? ? Hletin5)
 982                              [assumption
 983                              |intro;apply H5;inversion H8
 984                                 [intros;destruct;
 985                                  apply in_list_head
 986                                 |intros;destruct;
 987                                  do 2 apply in_list_cons;
 988                                  apply in_list_to_in_list_append_l;assumption]]
 989                           |elim (inlist_fv_swap ? ? ? ? ? H6)
 990                              [assumption
 991                              |intro;apply H5;elim (decidable_eq_nat a n4)
 992                                 [rewrite > H9;apply in_list_head
 993                                 |apply in_list_cons;
 994                                  inversion H8;intros;destruct;
 995                                    [apply in_list_head
 996                                    |apply in_list_cons;
 997                                     apply in_list_to_in_list_append_r;
 998                                     assumption]]]]]]]
 999               |apply in_list_head]
1000            |apply in_list_head]]]
1001 qed.
1002
1003 lemma encode_append : ∀T,U,n,l.length ? l ≤ n →
1004         subst_type_nat (encodetype T l) U n = encodetype T l.
1005 intros 2;elim T
1006   [simplify;elim (bool_to_decidable_eq (lookup n l) true)
1007      [rewrite > H1;simplify;lapply (lookup_in ? ? H1);
1008       lapply (posn_length ? ? Hletin);
1009       cut (posn l n ≠ n1)
1010         [rewrite > (not_eq_to_eqb_false ? ? Hcut);simplify;reflexivity
1011         |intro;rewrite > H2 in Hletin1;unfold in Hletin1;autobatch;]
1012      |cut (lookup n l = false)
1013         [rewrite > Hcut;reflexivity
1014         |generalize in match H1;elim (lookup n l);
1015            [elim H2;reflexivity|reflexivity]]]
1016   |simplify;reflexivity
1017   |simplify;autobatch
1018   |simplify;rewrite > (H ? ? H2);rewrite > H1
1019      [reflexivity
1020      |simplify;autobatch]]
1021 qed.
1022
1023 lemma encode_subst_simple : ∀X,T,l.
1024      (encodetype T l = subst_type_nat (encodetype T (l@[X])) (TFree X) (length ? l)).
1025 intros 2;elim T
1026   [simplify;cut (lookup n l = true → posn l n = posn (l@[X]) n)
1027      [generalize in match Hcut;elim (bool_to_decidable_eq (lookup n l) true)
1028         [cut (lookup n (l@[X]) = true)
1029            [rewrite > H;rewrite > Hcut1;simplify;
1030             cut (eqb (posn (l@[X]) n) (length nat l) = false)
1031               [rewrite > Hcut2;simplify;rewrite < (H1 H);reflexivity
1032               |generalize in match H;elim l 0
1033                  [simplify;intro;destruct H2
1034                  |intros 2;simplify;elim (eqb n t)
1035                     [simplify;reflexivity
1036                     |simplify in H3;simplify;apply (H2 H3)]]]
1037            |generalize in match H;elim l
1038               [simplify in H2;destruct H2
1039               |generalize in match H3;simplify;elim (eqb n t) 0
1040                  [simplify;intro;reflexivity
1041                  |simplify;intro;apply (H2 H4)]]]
1042         |cut (lookup n l = false)
1043            [elim (decidable_eq_nat n X)
1044               [rewrite > Hcut1;rewrite > H2;cut (lookup X (l@[X]) = true)
1045                  [rewrite > Hcut2;simplify;
1046                   cut (eqb (posn (l@[X]) X) (length nat l) = true)
1047                     [rewrite > Hcut3;simplify;reflexivity
1048                     |generalize in match Hcut1;elim l 0
1049                        [intros;simplify;rewrite > eqb_n_n;simplify;reflexivity
1050                        |simplify;intros 2;rewrite > H2;elim (eqb X t)
1051                           [simplify in H4;destruct H4
1052                           |simplify;simplify in H4;apply (H3 H4)]]]
1053                  |elim l
1054                     [simplify;rewrite > eqb_n_n;reflexivity
1055                     |simplify;elim (eqb X t)
1056                        [simplify;reflexivity
1057                        |simplify;assumption]]]
1058               |cut (lookup n l = lookup n (l@[X]))
1059                  [rewrite < Hcut2;rewrite > Hcut1;simplify;reflexivity
1060                  |elim l
1061                     [simplify;rewrite > (not_eq_to_eqb_false ? ? H2);simplify;
1062                      reflexivity
1063                     |simplify;elim (eqb n t)
1064                        [simplify;reflexivity
1065                        |simplify;assumption]]]]
1066            |generalize in match H;elim (lookup n l);
1067               [elim H2;reflexivity|reflexivity]]]
1068      |elim l 0
1069         [intro;simplify in H;destruct H
1070         |simplify;intros 2;elim (eqb n t)
1071            [simplify;reflexivity
1072            |simplify in H1;simplify;rewrite < (H H1);reflexivity]]]
1073   |simplify;reflexivity
1074   |simplify;rewrite < H;rewrite < H1;reflexivity
1075   |simplify;rewrite < H;rewrite < (append_associative ? [n] l [X]);
1076    rewrite < (H1 ([n]@l));reflexivity]
1077 qed.
1078
1079 lemma encode_subst : ∀T,X,Y,l.¬(X ∈ l) → ¬(Y ∈ l) →
1080                               (X ∈ (fv_NTyp T) → X = Y) →
1081                               encodetype (swap_NTyp X Y T) l =
1082                  subst_type_nat (encodetype T (l@[Y])) (TFree X) (length ? l).
1083 apply NTyp_len_ind;intro;elim U
1084   [elim (decidable_eq_nat n X)
1085      [rewrite > H4 in H3;rewrite > H4;rewrite > H3
1086         [simplify in \vdash (? ? (? % ?) ?);rewrite > swap_same;
1087          cut (lookup Y (l@[Y]) = true)
1088            [simplify;rewrite > Hcut;rewrite > (not_nat_in_to_lookup_false ? ? H2);
1089             simplify;cut (posn (l@[Y]) Y = length ? l)
1090               [rewrite > Hcut1;rewrite > eqb_n_n;reflexivity
1091               |generalize in match H2;elim l;simplify
1092                  [rewrite > eqb_n_n;reflexivity
1093                  |elim (decidable_eq_nat Y t)
1094                     [elim H6;rewrite > H7;apply in_list_head
1095                     |rewrite > (not_eq_to_eqb_false ? ? H7);simplify;
1096                      rewrite < H5
1097                        [reflexivity
1098                        |intro;apply H6;apply in_list_cons;assumption]]]]
1099            |elim l
1100               [simplify;rewrite > eqb_n_n;reflexivity
1101               |simplify;rewrite > H5;elim (eqb Y t);reflexivity]]
1102         |simplify;apply in_list_head]
1103      |elim (decidable_eq_nat Y n);
1104         [rewrite < H5;simplify;rewrite > swap_right;
1105          rewrite > (not_nat_in_to_lookup_false ? ? H1);
1106          cut (lookup Y (l@[Y]) = true)
1107            [rewrite > Hcut;simplify;cut (posn (l@[Y]) Y = length ? l)
1108               [rewrite > Hcut1;rewrite > eqb_n_n;reflexivity
1109               |generalize in match H2;elim l;simplify
1110                  [rewrite > eqb_n_n;reflexivity
1111                  |elim (decidable_eq_nat Y t)
1112                     [elim H7;rewrite > H8;apply in_list_head
1113                     |rewrite > (not_eq_to_eqb_false ? ? H8);simplify;
1114                      rewrite < H6
1115                        [reflexivity
1116                        |intro;apply H7;apply in_list_cons;assumption]]]]
1117            |elim l;simplify
1118                  [rewrite > eqb_n_n;reflexivity
1119                  |elim (eqb Y t);simplify;autobatch]]
1120         |simplify;rewrite > (swap_other X Y n)
1121            [cut (lookup n l = lookup n (l@[Y]) ∧
1122                  (lookup n l = true → posn l n = posn (l@[Y]) n))
1123               [elim Hcut;rewrite > H6;generalize in match H7;
1124                generalize in match H6;elim (lookup n (l@[Y]))
1125                  [simplify;rewrite < H9;generalize in match H8;elim l
1126                     [simplify in H10;destruct H10
1127                     |elim (decidable_eq_nat n t)
1128                        [simplify;rewrite > (eq_to_eqb_true ? ? H12);simplify;
1129                         reflexivity
1130                        |simplify;rewrite > (not_eq_to_eqb_false ? ? H12);
1131                         simplify;generalize in match H10;
1132                         elim (eqb (posn l1 n) (length nat l1))
1133                           [simplify in H13;simplify in H11;
1134                            rewrite > (not_eq_to_eqb_false ? ? H12) in H11;
1135                            simplify in H11;lapply (H13 H11);destruct Hletin
1136                           |simplify;reflexivity]]
1137                     |assumption
1138                     |assumption]
1139                  |simplify;reflexivity]
1140               |elim l;split
1141                  [simplify;cut (n ≠ Y)
1142                     [rewrite > (not_eq_to_eqb_false ? ? Hcut);simplify;
1143                      reflexivity
1144                     |intro;apply H5;symmetry;assumption]
1145                  |intro;simplify in H6;destruct H6
1146                  |elim H6;simplify;rewrite < H7;reflexivity
1147                  |simplify;elim (eqb n t)
1148                     [simplify;reflexivity
1149                     |simplify;simplify in H7;elim H6;rewrite < (H9 H7);
1150                      reflexivity]]]
1151            |assumption
1152            |intro;apply H5;symmetry;assumption]]]
1153   |simplify;reflexivity
1154   |simplify;rewrite < (H2 n ? ? ? ? H3 H4)
1155      [rewrite < (H2 n1 ? ? ? ? H3 H4);
1156         [autobatch|autobatch
1157         |intro;apply H5;simplify;apply in_list_to_in_list_append_r;assumption]
1158      |autobatch
1159      |intro;apply H5;simplify;apply in_list_to_in_list_append_l;assumption]
1160   |simplify;rewrite < (H2 n1 ? ? ? ? H3 H4)
1161      [cut (l = swap_list X Y l)
1162            [|generalize in match H3;generalize in match H4;elim l
1163                [simplify;reflexivity
1164                |simplify;elim (decidable_eq_nat t X)
1165                   [elim H8;rewrite > H9;apply in_list_head
1166                   |elim (decidable_eq_nat t Y)
1167                      [elim H7;rewrite > H10;apply in_list_head
1168                      |rewrite > (swap_other X Y t)
1169                         [rewrite < H6
1170                            [reflexivity
1171                            |intro;apply H7;apply in_list_cons;assumption
1172                            |intro;apply H8;apply in_list_cons;assumption]
1173                         |*:assumption]]]]]
1174       elim (decidable_eq_nat n Y)
1175         [rewrite > H6;rewrite > (fv_encode (swap_NTyp X Y n2) (swap X Y Y::l)
1176                       (swap_list X Y (Y::l)));
1177            [rewrite < (encode_swap X Y n2);
1178               [rewrite < (fv_encode ? (Y::l) (Y::l@[Y]))
1179                  [rewrite > encode_append;
1180                     [reflexivity(*rewrite < (fv_encode n2 (Y::l) (Y::l@[Y]));
1181                        [reflexivity
1182                        |intros;elim (decidable_eq_nat x Y)
1183                           [rewrite > H8;simplify;rewrite > eqb_n_n;simplify;
1184                            split [reflexivity|intro;reflexivity]
1185                           |simplify;rewrite > (not_eq_to_eqb_false ? ? H8);
1186                            simplify;elim l
1187                              [simplify;rewrite > (not_eq_to_eqb_false ? ? H8);
1188                               simplify;split [reflexivity|intro;destruct H9]
1189                              |elim H9;simplify;elim (eqb x t)
1190                                 [simplify;split [reflexivity|intro;reflexivity]
1191                                 |simplify;rewrite < H10;generalize in match H11;
1192                                  elim (lookup x l1)
1193                                    [split
1194                                       [reflexivity
1195                                       |intro;rewrite < (H12 H13);reflexivity]
1196                                    |split [reflexivity|intro;destruct H13]]]]]]*)
1197                     |simplify;constructor 1]
1198                  |intros;simplify;elim (decidable_eq_nat x Y)
1199                     [rewrite > (eq_to_eqb_true ? ? H8);simplify;split
1200                        [reflexivity|intro;reflexivity]
1201                     |rewrite > (not_eq_to_eqb_false ? ? H8);simplify;elim l
1202                        [simplify;rewrite > (not_eq_to_eqb_false ? ? H8);
1203                         simplify;split [reflexivity|intro;destruct H9]
1204                        |simplify;elim (eqb x t)
1205                           [simplify;split [reflexivity|intro;reflexivity]
1206                           |simplify;elim H9;split
1207                              [assumption
1208                              |intro;rewrite < (H11 H12);reflexivity]]]]]
1209               |intro;elim (decidable_eq_nat X Y)
1210                  [rewrite > H8;apply in_list_head
1211                  |elim H8;apply H5;simplify;apply in_list_to_in_list_append_r;
1212                   rewrite > H6;apply (in_remove ? ? ? H8 H7)]
1213               |apply in_list_head]
1214            |intros;simplify;rewrite > swap_right;rewrite < Hcut;
1215             split [reflexivity|intro;reflexivity]]
1216         |(*rewrite < Hcut;*)elim (decidable_eq_nat n X)
1217            [rewrite > H7;rewrite > (fv_encode (swap_NTyp X Y n2) (swap X Y X::l)
1218                          (swap_list X Y (X::l)))
1219               [rewrite > (encode_swap X Y n2);
1220                  [simplify;
1221                   cut (swap X Y X::swap_list X Y (l@[Y]) =
1222                         (swap X Y X::swap_list X Y l)@[X])
1223                     [rewrite > Hcut1;cut (S (length ? l) = (length ? (swap X Y X::swap_list X Y l)))
1224                        [rewrite > Hcut2;rewrite < (encode_subst_simple X
1225                               (swap_NTyp X Y n2) (swap X Y X::swap_list X Y l));
1226                         reflexivity
1227                        |simplify;elim l
1228                           [reflexivity
1229                           |simplify;rewrite < H8;reflexivity]]
1230                     |simplify;elim l
1231                        [simplify;rewrite > swap_right;reflexivity
1232                        |simplify;destruct;rewrite > Hcut1;reflexivity]]
1233                  |intro;apply in_list_head
1234                  |apply in_list_cons;elim l
1235                     [simplify;apply in_list_head
1236                     |simplify;apply in_list_cons;assumption]]
1237               |intros;simplify;rewrite < Hcut;
1238                split [reflexivity|intro;reflexivity]]
1239            |rewrite > (swap_other X Y n)
1240               [rewrite < (append_associative ? [n] l [Y]);
1241                cut (S (length nat l) = length nat (n::l)) [|reflexivity]
1242                rewrite > Hcut1;rewrite < (H2 n2);
1243                  [reflexivity
1244                  |autobatch
1245                  |intro;apply H7;inversion H8;intros
1246                     [destruct;reflexivity
1247                     |destruct;elim (H3 H9)]
1248                  |intro;apply H6;inversion H8;intros
1249                     [destruct;reflexivity
1250                     |destruct;elim (H4 H9)]
1251                  |intro;apply H5;simplify;apply in_list_to_in_list_append_r;
1252                   apply (in_remove ? ? ? ? H8);intro;apply H7;symmetry;assumption]
1253               |*:assumption]]]
1254      |autobatch
1255      |intro;apply H5;simplify;apply in_list_to_in_list_append_l;assumption]]
1256 qed.
1257
1258 lemma swap_case: ∀u,v,x.(swap u v x) = u ∨ (swap u v x) = v ∨ (swap u v x = x).
1259 intros.unfold in match swap.simplify.elim (eqb x u)
1260   [simplify;autobatch
1261   |simplify;elim (eqb x v);simplify;autobatch]
1262 qed.
1263
1264 lemma in_fvNTyp_in_fvNenv : ∀G,T.(NWFType G T) → (incl ? (fv_NTyp T) (fv_Nenv G)).
1265 intros;elim H
1266   [simplify;unfold;intros;inversion H2;intros
1267      [destruct;assumption
1268      |destruct;elim (not_in_list_nil ? ? H3)]
1269   |simplify;unfold;intros;elim (not_in_list_nil ? ? H1)
1270   |simplify;unfold;intros;elim (in_list_append_to_or_in_list ? ? ? ? H5)
1271      [apply (H2 ? H6)|apply (H4 ? H6)]
1272   |simplify;unfold;intros;elim (in_list_append_to_or_in_list ? ? ? ? H5)
1273      [apply H2;assumption
1274      |elim (fresh_name (x::fv_Nenv l@var_NTyp n2));lapply (H4 a)
1275         [cut (a ≠ x ∧ x ≠ n)
1276            [elim Hcut;lapply (Hletin x)
1277               [simplify in Hletin1;inversion Hletin1;intros;
1278                  [destruct;elim H8;reflexivity
1279                  |destruct;assumption]
1280               |generalize in match H6;generalize in match H7;elim n2
1281                  [simplify in H11;elim (decidable_eq_nat n n3)
1282                     [rewrite > (eq_to_eqb_true ? ? H12) in H11;simplify in H11;
1283                      elim (not_in_list_nil ? ? H11)
1284                     |rewrite > (not_eq_to_eqb_false ? ? H12) in H11;
1285                      simplify in H11;inversion H11;intros
1286                        [destruct;simplify;
1287                         rewrite > swap_other
1288                           [apply in_list_head
1289                           |intro;apply H8;rewrite > H13;reflexivity
1290                           |intro;apply H9;rewrite > H13;reflexivity]
1291                        |destruct;elim (not_in_list_nil ? ? H13)]]
1292                  |simplify in H11;elim (not_in_list_nil ? ? H11)
1293                  |simplify in H13;simplify;elim (remove_inlist ? ? ? H13);
1294                   elim (in_list_append_to_or_in_list ? ? ? ? H14)
1295                     [apply in_list_to_in_list_append_l;apply H10
1296                        [intro;apply H12;simplify;
1297                         rewrite < (append_associative ? [x] (fv_Nenv l) (var_NTyp n3 @ var_NTyp n4));
1298                         elim (in_list_append_to_or_in_list ? ? (x::fv_Nenv l) (var_NTyp n3) H17);
1299                           [apply in_list_to_in_list_append_l;assumption
1300                           |apply in_list_to_in_list_append_r;
1301                            apply in_list_to_in_list_append_l;assumption]
1302                        |apply (in_remove ? ? ? H15 H16)]
1303                     |apply in_list_to_in_list_append_r;apply H11
1304                        [intro;apply H12;simplify;
1305                         rewrite < (append_associative ? [x] (fv_Nenv l) (var_NTyp n3 @ var_NTyp n4));
1306                         elim (in_list_append_to_or_in_list ? ? (x::fv_Nenv l) (var_NTyp n4) H17);
1307                           [apply in_list_to_in_list_append_l;assumption
1308                           |apply in_list_to_in_list_append_r;
1309                            apply in_list_to_in_list_append_r;assumption]
1310                        |apply (in_remove ? ? ? H15 H16)]]
1311                  |simplify;simplify in H13;elim (remove_inlist ? ? ? H13);
1312                   elim (nat_in_list_case ? ? ? H14);
1313                     [apply in_list_to_in_list_append_r;apply in_remove;
1314                        [elim (remove_inlist ? ? ? H16);intro;apply H18;
1315                         elim (swap_case a n n3)
1316                           [elim H20
1317                              [elim H8;symmetry;rewrite < H21;assumption
1318                              |elim H9;rewrite < H21;assumption]
1319                           |rewrite < H20;assumption]
1320                        |apply H11;
1321                           [rewrite < (append_associative ? [x] (fv_Nenv l) (var_NTyp n5));
1322                            intro;apply H12;simplify;
1323                            rewrite < (append_associative ? [x] (fv_Nenv l) (n3::var_NTyp n4 @ var_NTyp n5));
1324                            elim (nat_in_list_case ? ? ? H17)
1325                              [apply in_list_to_in_list_append_r;
1326                               apply in_list_cons;
1327                               apply in_list_to_in_list_append_r;assumption
1328                              |apply in_list_to_in_list_append_l;assumption]
1329                           |elim (remove_inlist ? ? ? H16);apply in_remove
1330                              [assumption
1331                              |assumption]]]
1332                     |apply in_list_to_in_list_append_l;apply H10;
1333                        [rewrite < (append_associative ? [x] (fv_Nenv l) (var_NTyp n4));
1334                         intro;apply H12;simplify;
1335                         rewrite < (append_associative ? [x] (fv_Nenv l) (n3::var_NTyp n4@var_NTyp n5));
1336                         elim (nat_in_list_case ? ? ? H17)
1337                           [apply in_list_to_in_list_append_r;apply in_list_cons;
1338                            apply in_list_to_in_list_append_l;assumption
1339                           |apply in_list_to_in_list_append_l;assumption]
1340                        |apply in_remove;assumption]]]]
1341            |split
1342               [intro;apply H7;rewrite > H8;apply in_list_head
1343               |elim (remove_inlist ? ? ? H6);assumption]]
1344         |intro;apply H7;apply in_list_cons;apply in_list_to_in_list_append_l;
1345          assumption
1346         |right;intro;apply H7;apply in_list_cons;
1347          apply in_list_to_in_list_append_r;apply (incl_fv_var ? ? H8)]]]
1348 qed.
1349
1350 lemma fv_NTyp_fv_Typ : ∀T,X,l.(X ∈ (fv_NTyp T)) → ¬(X ∈ l) →
1351                           (X ∈ (fv_type (encodetype T l))).
1352 intros 2;elim T
1353   [simplify;simplify in H;cut (X = n)
1354      [rewrite < Hcut;generalize in match (lookup_in X l);elim (lookup X l)
1355         [elim H1;apply H2;reflexivity
1356         |simplify;apply in_list_head]
1357      |(*FIXME*)generalize in match H;intro;inversion H;intros;
1358         [destruct;reflexivity
1359         |destruct;elim (not_in_list_nil ? ? H3)]]
1360   |simplify in H;elim (not_in_list_nil ? ? H)
1361   |simplify;simplify in H2;
1362    elim (in_list_append_to_or_in_list ? ? ? ? H2);
1363      [apply in_list_to_in_list_append_l;apply (H ? H4 H3)
1364      |apply in_list_to_in_list_append_r;apply (H1 ? H4 H3)]
1365   |simplify;simplify in H2;
1366    elim (in_list_append_to_or_in_list ? ? ? ? H2)
1367      [apply in_list_to_in_list_append_l;apply (H ? H4 H3)
1368      |apply in_list_to_in_list_append_r;
1369       elim (remove_inlist ? ? ? H4);apply (H1 ? H5);intro;apply H6;
1370       inversion H7;intros
1371         [destruct;reflexivity
1372         |destruct;elim (H3 H8)]]]
1373 qed.
1374
1375 lemma adeq_WFT : ∀G,T.NWFType G T → WFType (encodeenv G) (encodetype T []).
1376 intros;elim H
1377   [simplify;apply WFT_TFree;rewrite < eq_fv_Nenv_fv_env;assumption
1378   |simplify;apply WFT_Top;
1379   |simplify;apply WFT_Arrow;assumption
1380   |simplify;apply WFT_Forall
1381      [assumption
1382      |intros;rewrite < (encode_subst n2 X n []);
1383         [simplify in H4;apply H4
1384            [rewrite > (eq_fv_Nenv_fv_env l);assumption
1385            |elim (decidable_eq_nat X n)
1386               [left;assumption
1387               |right;intro;apply H6;apply (fv_NTyp_fv_Typ ? ? ? H8);intro;
1388                apply H7;inversion H9;intros
1389                  [destruct;reflexivity
1390                  |destruct;
1391                   elim (not_in_list_nil ? ? H10)]]]
1392         |4:intro;elim (decidable_eq_nat X n)
1393            [assumption
1394            |elim H6;cut (¬(X ∈ [n]))
1395               [generalize in match Hcut;generalize in match [n];
1396                generalize in match H7;elim n2
1397                  [simplify in H9;generalize in match H9;intro;inversion H9;intros;
1398                     [destruct;simplify;
1399                      generalize in match (lookup_in X l1);elim (lookup X l1)
1400                        [elim H10;apply H12;reflexivity
1401                        |simplify;apply in_list_head]
1402                     |destruct;
1403                      elim (not_in_list_nil ? ? H12)]
1404                  |simplify in H9;elim (not_in_list_nil ? ? H9)
1405                  |simplify;simplify in H11;
1406                   elim (in_list_append_to_or_in_list ? ? ? ? H11);autobatch
1407                  |simplify;simplify in H11;
1408                   elim (in_list_append_to_or_in_list ? ? ? ? H11);
1409                     [autobatch
1410                     |elim (remove_inlist ? ? ? H13);
1411                      apply in_list_to_in_list_append_r;
1412                      apply (H10 H14);
1413                      intro;inversion H16;intros;
1414                        [destruct;elim H15;reflexivity
1415                        |destruct;elim H12;assumption]]]
1416               |intro;elim H8;inversion H9;intros
1417                  [destruct;autobatch
1418                  |destruct;elim (not_in_list_nil ? ? H10)]]]
1419         |*:apply not_in_list_nil]]]
1420 qed.
1421
1422 lemma not_in_list_encodetype : \forall T,l,x.in_list ? x l \to
1423                       \lnot (in_list ? x (fv_type (encodetype T l))).
1424 intro;elim T;simplify
1425   [apply (bool_elim ? (lookup n l));intro
1426      [simplify;apply not_in_list_nil
1427      |simplify;intro;inversion H2;intros
1428         [destruct;
1429          rewrite > (in_lookup ? ? H) in H1;destruct H1
1430         |destruct;apply (not_in_list_nil ? ? H3)]]
1431   |apply not_in_list_nil
1432   |intro;elim (nat_in_list_case ? ? ? H3)
1433      [apply H1;assumption
1434      |apply H;assumption]
1435   |intro;elim (nat_in_list_case ? ? ? H3)
1436      [apply (H1 (n::l) x ? H4);apply in_list_cons;assumption
1437      |apply H;assumption]]
1438 qed.
1439
1440 lemma incl_fv_encode_fv : \forall T,l.incl ? (fv_type (encodetype T l)) (fv_NTyp T).
1441 intro;elim T;simplify;unfold;
1442   [intro;elim (lookup n l)
1443      [simplify in H;elim (not_in_list_nil ? ? H)
1444      |simplify in H;assumption]
1445   |intros;elim (not_in_list_nil ? ? H)
1446   |intros;elim (in_list_append_to_or_in_list ? ? ? ? H2)
1447      [apply in_list_to_in_list_append_l;apply H;autobatch
1448      |apply in_list_to_in_list_append_r;apply H1;autobatch]
1449   |intros;elim (in_list_append_to_or_in_list ? ? ? ? H2)
1450      [apply in_list_to_in_list_append_l;apply H;autobatch
1451      |apply in_list_to_in_list_append_r;apply in_remove
1452         [intro;apply (not_in_list_encodetype n2 (n::l) x)
1453            [rewrite > H4;apply in_list_head
1454            |assumption]
1455         |apply (H1 (n::l));assumption]]]
1456 qed.
1457
1458 lemma adeq_WFT2 : ∀G1,T1.WFType G1 T1 →
1459                      ∀G2,T2.G1 = encodeenv G2 → T1 = encodetype T2 [] →
1460                    NWFType G2 T2.
1461 intros 3;elim H
1462   [rewrite > H2 in H1;rewrite < eq_fv_Nenv_fv_env in H1;
1463    cut (T2 = TName n)
1464      [|generalize in match H3;elim T2
1465         [simplify in H4;destruct;reflexivity
1466         |simplify in H4;destruct H4
1467         |simplify in H6;destruct H6
1468         |simplify in H6;destruct H6]]
1469    rewrite > Hcut;apply NWFT_TName;assumption
1470   |cut (T2 = NTop)
1471      [|generalize in match H2;elim T2
1472         [simplify in H3;destruct H3
1473         |reflexivity
1474         |simplify in H5;destruct H5
1475         |simplify in H5;destruct H5]]
1476    rewrite > Hcut;apply NWFT_Top;
1477   |cut (∃U,V.T2 = (NArrow U V))
1478      [|generalize in match H6;elim T2
1479         [1,2:simplify in H7;destruct H7
1480         |apply (ex_intro ? ? n);apply (ex_intro ? ? n1);reflexivity
1481         |simplify in H9;destruct H9]]
1482    elim Hcut;elim H7;rewrite > H8 in H6;simplify in H6;destruct;
1483    apply NWFT_Arrow;autobatch
1484   |cut (\exists Z,U,V.T2 = NForall Z U V)
1485      [|generalize in match H6;elim T2
1486         [1,2:simplify in H7;destruct H7
1487         |simplify in H9;destruct H9
1488         |apply (ex_intro ? ? n);apply (ex_intro ? ? n1);
1489          apply (ex_intro ? ? n2);reflexivity]]
1490    elim Hcut;elim H7;elim H8;clear Hcut H7 H8;rewrite > H9;
1491    rewrite > H9 in H6;simplify in H6;destruct;apply NWFT_Forall
1492      [autobatch
1493      |intros;elim H6
1494         [rewrite > H7;cut (swap_NTyp a a a2 = a2)
1495            [|elim a2;simplify
1496               [rewrite > swap_same;reflexivity
1497               |reflexivity
1498               |rewrite > H8;rewrite > H9;reflexivity
1499               |rewrite > swap_same;rewrite > H8;rewrite > H9;reflexivity]]
1500          rewrite > Hcut;apply (H4 Y)
1501            [rewrite < eq_fv_Nenv_fv_env;assumption
1502            |rewrite > H7;apply not_in_list_encodetype;
1503             apply in_list_head
1504            |rewrite > H7;simplify;reflexivity
1505            |rewrite > H7;autobatch]
1506         |apply (H4 Y)
1507            [rewrite < eq_fv_Nenv_fv_env;assumption
1508            |intro;apply H7;apply incl_fv_encode_fv;autobatch
1509            |simplify;reflexivity
1510            |symmetry;apply (encode_subst a2 Y a []);
1511               [3:intro;elim (H7 H8)
1512               |*:autobatch]]]]]
1513 qed.
1514
1515 lemma adeq_WFE : ∀G.NWFEnv G → WFEnv (encodeenv G).
1516 intros;elim H
1517   [simplify;apply WFE_Empty
1518   |simplify;apply WFE_cons;
1519      [2:rewrite < eq_fv_Nenv_fv_env;]
1520    autobatch]
1521 qed.
1522
1523 lemma NWFT_env_incl : ∀G,T.NWFType G T → ∀H.incl ? (fv_Nenv G) (fv_Nenv H)
1524                       → NWFType H T.
1525 intros 3;elim H
1526   [apply NWFT_TName;apply (H3 ? H1)
1527   |apply NWFT_Top
1528   |apply NWFT_Arrow
1529      [apply (H2 ? H6)
1530      |apply (H4 ? H6)]
1531   |apply NWFT_Forall
1532      [apply (H2 ? H6)
1533      |intros;apply (H4 ? ? H8);
1534         [intro;apply H7;apply (H6 ? H9)
1535         |unfold;intros;simplify;simplify in H9;inversion H9;intros
1536            [destruct;apply in_list_head
1537            |destruct;apply in_list_cons;apply (H6 ? H10)]]]]
1538 qed.
1539
1540 (*lemma NWFT_subst :
1541   \forall T,U,a,X,Y,G.
1542     NWFType (mk_nbound true a U::G) (swap_NTyp a X T) \to
1543     \lnot (in_list ? a (Y::X::fv_NTyp T@fv_Nenv G)) \to
1544     \lnot (in_list ? Y (fv_Nenv G)) \to
1545     (Y = X \lor \lnot (in_list ? Y (fv_NTyp T))) \to
1546     NWFType (mk_nbound true Y U::G) (swap_NTyp Y X T).
1547 apply NTyp_len_ind;intro;cases U
1548   [4:simplify;intros;apply NWFT_Forall
1549      [
1550      |intros;apply (H ? ? ? Y)
1551         [2:inversion H1;simplify;intros;destruct;
1552            [
1553
1554 intros 7;elim T
1555   [4:simplify;apply NWFT_Forall
1556      [
1557      |intros;*)
1558
1559
1560 lemma NJSubtype_to_NWFT : ∀G,T,U.NJSubtype G T U → NWFType G T ∧ NWFType G U.
1561 intros;elim H
1562   [split [assumption|apply NWFT_Top]
1563   |split;apply NWFT_TName;assumption
1564   |elim H3;split;
1565      [apply NWFT_TName;generalize in match H1;elim l
1566         [elim (not_in_list_nil ? ? H6)
1567         |inversion H7;intros
1568            [rewrite < H8;simplify;apply in_list_head
1569            |destruct;elim t;simplify;apply in_list_cons;
1570             apply H6;assumption]]
1571      |assumption]
1572   |elim H2;elim H4;split;apply NWFT_Arrow;assumption
1573   |split;assumption
1574   |elim H2;split
1575      [lapply (adeq_WFT ? ? H5);apply (adeq_WFT2 ? ? Hletin);autobatch
1576      |lapply (adeq_WFT ? ? H6);apply (adeq_WFT2 ? ? Hletin);autobatch]]
1577 qed.
1578
1579 theorem adequacy : ∀G,T,U.NJSubtype G T U →
1580                     JSubtype (encodeenv G) (encodetype T []) (encodetype U []).
1581 intros;elim H;simplify
1582   [1,3,4:autobatch
1583   |apply SA_Refl_TVar
1584      [apply (adeq_WFE ? H1)|rewrite < eq_fv_Nenv_fv_env;assumption]
1585   |apply SA_All
1586      [assumption
1587      |intros;lapply (NSA_All ? ? ? ? ? ? ? H1 H2 H3 H5);
1588       rewrite < (encode_subst n3 X n [])
1589         [rewrite < (encode_subst n5 X n1 [])
1590            [rewrite < eq_fv_Nenv_fv_env in H7;
1591             elim (NJSubtype_to_NWFT ? ? ? Hletin);
1592             lapply (in_fvNTyp_in_fvNenv ? ? H8);
1593             lapply (in_fvNTyp_in_fvNenv ? ? H9);
1594             simplify in Hletin1;simplify in Hletin2;
1595             apply (H6 ? H7)
1596               [elim (decidable_eq_nat X n)
1597                  [left;assumption
1598                  |right;intro;lapply (in_remove ? ? ? H10 H11);elim H7;
1599                   apply Hletin1;apply in_list_to_in_list_append_r;assumption]
1600               |elim (decidable_eq_nat X n1)
1601                  [left;assumption
1602                  |right;intro;lapply (in_remove ? ? ? H10 H11);elim H7;
1603                   apply Hletin2;apply in_list_to_in_list_append_r;assumption]]
1604            |2,3:apply not_in_list_nil
1605            |intro;elim (NJSubtype_to_NWFT ? ? ? Hletin);
1606             lapply (in_fvNTyp_in_fvNenv ? ? H10);simplify in Hletin1;
1607             elim (decidable_eq_nat X n1)
1608               [assumption
1609               |lapply (in_remove ? ? ? H11 H8);elim H7;rewrite < eq_fv_Nenv_fv_env;
1610                apply Hletin1;apply in_list_to_in_list_append_r;assumption]]
1611         |2,3:apply not_in_list_nil
1612         |intro;elim (NJSubtype_to_NWFT ? ? ? Hletin);lapply (in_fvNTyp_in_fvNenv ? ? H9);
1613          simplify in Hletin1;elim (decidable_eq_nat X n)
1614            [assumption
1615            |lapply (in_remove ? ? ? H11 H8);elim H7;rewrite < eq_fv_Nenv_fv_env;
1616             apply Hletin1;apply in_list_to_in_list_append_r;assumption]]]
1617   |rewrite < (alpha_to_encode ? ? H3);rewrite < (alpha_to_encode ? ? H4);
1618    assumption]
1619 qed.
1620
1621 let rec closed_type T n ≝
1622   match T with
1623     [ TVar m ⇒ m < n
1624     | TFree X ⇒ True
1625     | Top ⇒ True
1626     | Arrow T1 T2 ⇒ closed_type T1 n ∧ closed_type T2 n
1627     | Forall T1 T2 ⇒  closed_type T1 n ∧ closed_type T2 (S n)].
1628
1629 alias id "nth" = "cic:/matita/list/list/nth.con".
1630 alias id "length" = "cic:/matita/list/list/length.con".
1631 definition distinct_list ≝
1632 λl.∀n,m.n < length ? l → m < length ? l → n ≠ m → nth ? l O n ≠ nth ? l O m.
1633
1634 lemma posn_nth: ∀l,n.distinct_list l → n < length ? l →
1635                     posn l (nth ? l O n) = n.
1636 intro;elim l
1637   [simplify in H1;elim (not_le_Sn_O ? H1)
1638   |simplify in H2;generalize in match H2;elim n
1639      [simplify;rewrite > eqb_n_n;simplify;reflexivity
1640      |simplify;cut (nth ? (t::l1) O (S n1) ≠ nth ? (t::l1) O O)
1641         [simplify in Hcut;rewrite > (not_eq_to_eqb_false ? ? Hcut);simplify;
1642          rewrite > (H n1)
1643            [reflexivity
1644            |unfold;intros;unfold in H1;lapply (H1 (S n2) (S m));
1645               [simplify in Hletin;assumption
1646               |2,3:simplify;autobatch
1647               |intro;apply H7;destruct H8;reflexivity]
1648            |autobatch]
1649         |intro;apply H1;
1650            [6:apply H5
1651            |skip
1652            |skip
1653            |*:autobatch]]]]
1654 qed.
1655
1656 lemma nth_in_list : ∀l,n. n < length ? l → nth ? l O n ∈ l.
1657 intro;elim l
1658   [simplify in H;elim (not_le_Sn_O ? H)
1659   |generalize in match H1;elim n
1660      [simplify;apply in_list_head
1661      |simplify;apply in_list_cons;apply H;simplify in H3;apply (le_S_S_to_le ? ? H3)]]
1662 qed.
1663
1664 lemma lookup_nth : \forall l,n.n < length ? l \to
1665                    lookup (nth nat l O n) l = true.
1666 intro;elim l
1667   [elim (not_le_Sn_O ? H);
1668   |generalize in match H1;elim n
1669      [simplify;rewrite > eqb_n_n;reflexivity
1670      |simplify;elim (eqb (nth nat l1 O n1) t)
1671         [reflexivity
1672         |simplify;apply H;apply le_S_S_to_le;assumption]]]
1673 qed.
1674
1675 lemma decoder : ∀T,n.closed_type T n →
1676                      ∀l.length ? l = n → distinct_list l →
1677                   (\forall x. in_list ? x (fv_type T) \to \lnot in_list ? x l) \to
1678                      ∃U.T = encodetype U l.
1679 intro;elim T
1680   [simplify in H;apply (ex_intro ? ? (TName (nth ? l O n)));simplify;
1681    rewrite > lookup_nth
1682      [simplify;rewrite > posn_nth;
1683         [reflexivity|assumption|rewrite > H1;assumption]
1684      |rewrite > H1;assumption]
1685   |apply (ex_intro ? ? (TName n));rewrite > (fv_encode (TName n) l []);
1686      [simplify;reflexivity
1687      |intros;simplify in H3;simplify in H4;lapply (H3 ? H4);
1688       cut (lookup x l = false)
1689         [rewrite > Hcut;simplify;split
1690            [reflexivity|intro;destruct H5]
1691         |elim (bool_to_decidable_eq (lookup x l) true)
1692            [lapply (lookup_in ? ? H5);elim (Hletin Hletin1)
1693            |generalize in match H5;elim (lookup x l);
1694               [elim H6;reflexivity|reflexivity]]]]
1695   |apply (ex_intro ? ? NTop);simplify;reflexivity
1696   |simplify in H2;elim H2;lapply (H ? H6 ? H3 H4);
1697      [lapply (H1 ? H7 ? H3 H4)
1698         [elim Hletin;elim Hletin1;
1699          apply (ex_intro ? ? (NArrow a a1));simplify;
1700          rewrite < H9;rewrite < H8;reflexivity
1701         |intros;apply H5;simplify;apply in_list_to_in_list_append_r;assumption]
1702      |intros;apply H5;simplify;apply in_list_to_in_list_append_l;assumption]
1703   |simplify in H2;elim H2;elim (H ? H6 ? H3 H4);elim (fresh_name (fv_type t1@l));
1704      [elim (H1 ? H7 (a1::l))
1705         [apply (ex_intro ? ? (NForall a1 a a2));simplify;rewrite < H8;rewrite < H10;
1706          reflexivity
1707         |simplify;rewrite > H3;reflexivity
1708         |unfold;intros;intro;apply H12;generalize in match H13;generalize in match H10;
1709          generalize in match H11;generalize in match H9;
1710          generalize in match m;generalize in match n1;
1711          apply nat_elim2
1712            [intro;elim n2
1713               [reflexivity
1714               |simplify in H18;rewrite > H18 in H9;elim H9;simplify in H16;
1715                lapply (le_S_S_to_le ? ? H16);apply in_list_to_in_list_append_r;
1716                autobatch]
1717            |intro;intros;change in H17:(? ? % ?) with (nth nat l O n2);
1718             simplify in H17:(? ? ? %);elim H9;rewrite < H17;
1719             apply in_list_to_in_list_append_r;apply nth_in_list;
1720             simplify in H16;apply (le_S_S_to_le ? ? H16)
1721            |intros;change in H18 with (nth nat l O n2 = nth nat l O m1);
1722             unfold in H4;elim (decidable_eq_nat n2 m1)
1723               [rewrite > H19;reflexivity
1724               |simplify in H17;simplify in H16;elim (H4 ? ? ? ? H19)
1725                  [assumption
1726                  |apply (le_S_S_to_le ? ? H17)
1727                  |apply (le_S_S_to_le ? ? H16)]]]
1728         |intro;elim (in_list_cons_case ? ? ? ? H11)
1729            [apply H9;apply in_list_to_in_list_append_l;rewrite < H12;assumption
1730            |apply (H5 x)
1731               [simplify;apply in_list_to_in_list_append_r;assumption
1732               |assumption]]]
1733      |apply H5;simplify;apply in_list_to_in_list_append_l;assumption]]
1734 qed.
1735
1736 lemma closed_subst : \forall T,X,n.closed_type (subst_type_nat T (TFree X) n) n
1737                      \to closed_type T (S n).
1738 intros 2;elim T 0;simplify;intros
1739   [elim (decidable_eq_nat n n1)
1740      [rewrite > H1;apply le_n
1741      |rewrite > (not_eq_to_eqb_false ? ? H1) in H;simplify in H;
1742       apply le_S;assumption]
1743   |2,3:apply I
1744   |elim H2;split;autobatch
1745   |elim H2;split;autobatch]
1746 qed.
1747
1748 lemma WFT_to_closed: ∀G,T.WFType G T → closed_type T O.
1749 intros;elim H;simplify
1750   [apply I
1751   |apply I
1752   |split;assumption
1753   |split
1754      [assumption
1755      |elim (fresh_name (fv_env l@fv_type t1));lapply (H4 a)
1756         [autobatch
1757         |intro;apply H5;apply in_list_to_in_list_append_l;assumption
1758         |intro;apply H5;apply in_list_to_in_list_append_r;assumption]]]
1759 qed.
1760
1761 lemma adeq_WFE2 : ∀G1.WFEnv G1 → ∀G2.(G1 = encodeenv G2) → NWFEnv G2.
1762 intros 2;elim H 0
1763   [intro;elim G2
1764      [apply NWFE_Empty
1765      |simplify in H2;destruct H2]
1766   |intros 9;elim G2
1767      [simplify in H5;destruct H5
1768      |generalize in match H6;elim t1;simplify in H7;destruct H7;apply NWFE_cons
1769         [apply H2;reflexivity
1770         |rewrite > eq_fv_Nenv_fv_env;assumption
1771         |autobatch]]]
1772 qed.
1773
1774 lemma xxx : \forall b,X,T,l.
1775             in_list ? (mk_bound b X (encodetype T [])) (encodeenv l) \to
1776             \exists U.encodetype U [] = encodetype T [] \land
1777                       in_list ? (mk_nbound b X U) l.
1778 intros 4;elim l
1779   [simplify in H;elim (not_in_list_nil ? ? H)
1780   |simplify in H1;inversion H1;elim t 0;simplify;intros;destruct;
1781      [apply (ex_intro ? ? n1);split;autobatch
1782      |elim (H H2);elim H4;apply (ex_intro ? ? a);split;autobatch]]
1783 qed.
1784
1785 lemma eq_swap_NTyp_to_case :
1786   \forall X,Y,Z,T.\lnot in_list ? Y (X::var_NTyp T) \to
1787     swap_NTyp Z Y (swap_NTyp Y X T) = swap_NTyp Z X T \to
1788       Z = X \lor \lnot in_list ? Z (fv_NTyp T).
1789 intros 4;elim T
1790   [simplify in H;simplify in H1;elim (decidable_eq_nat X n)
1791      [rewrite > H2;simplify;elim (decidable_eq_nat Z n)
1792         [left;assumption
1793         |right;intro;apply H3;apply in_list_singleton_to_eq;assumption]
1794      |elim (decidable_eq_nat Y n)
1795         [elim H;rewrite > H3;apply in_list_cons;apply in_list_head
1796         |rewrite > (swap_other Y X n) in H1
1797            [elim (decidable_eq_nat Z n)
1798               [rewrite > H4 in H1;do 2 rewrite > swap_left in H1;
1799                destruct H1;elim H;apply in_list_head
1800               |elim (decidable_eq_nat Z X)
1801                  [left;assumption
1802                  |rewrite > (swap_other Z X n) in H1
1803                     [right;intro;apply H3;simplify in H6;
1804                      rewrite > (in_list_singleton_to_eq ? ? ? H6) in H1;
1805                      rewrite > swap_left in H1;destruct H1;reflexivity
1806                     |intro;apply H4;symmetry;assumption
1807                     |intro;apply H2;symmetry;assumption]]]
1808            |intro;apply H3;symmetry;assumption
1809            |intro;apply H2;symmetry;assumption]]]
1810   |simplify;right;apply not_in_list_nil
1811   |elim H
1812      [left;assumption
1813      |elim H1
1814         [left;assumption
1815         |right;simplify;intro;elim (in_list_append_to_or_in_list ? ? ? ? H6)
1816            [elim (H4 H7)
1817            |elim (H5 H7)]
1818         |intro;apply H2;simplify;inversion H5;intros;destruct;
1819            [apply in_list_head
1820            |apply in_list_cons;apply in_list_to_in_list_append_r;assumption]
1821         |simplify in H3;destruct H3;assumption]
1822      |intro;apply H2;simplify;inversion H4;intros;destruct;
1823         [apply in_list_head
1824         |apply in_list_cons;apply in_list_to_in_list_append_l;assumption]
1825      |simplify in H3;destruct H3;assumption]
1826   |elim H
1827      [left;assumption
1828      |elim H1
1829         [left;assumption
1830         |right;simplify;intro;elim (in_list_append_to_or_in_list ? ? ? ? H6)
1831            [elim (H4 H7)
1832            |elim H5;elim (remove_inlist ? ? ? H7);assumption]
1833         |intro;apply H2;simplify;inversion H5;intros;destruct;
1834            [apply in_list_head
1835            |do 2 apply in_list_cons;apply in_list_to_in_list_append_r;assumption]
1836         |simplify in H3;destruct H3;assumption]
1837      |intro;apply H2;simplify;inversion H4;intros;destruct;
1838         [apply in_list_head
1839         |do 2 apply in_list_cons;apply in_list_to_in_list_append_l;assumption]
1840      |simplify in H3;destruct H3;assumption]]
1841 qed.
1842
1843
1844 theorem faithfulness : ∀G1,T1,U1.G1 ⊢ T1 ⊴ U1 →
1845                           ∀G2,T2,U2.
1846                        G1 = encodeenv G2 →
1847                        T1 = encodetype T2 [] →
1848                        U1 = encodetype U2 [] →
1849                        NJSubtype G2 T2 U2.
1850 intros 4;elim H 0
1851   [intros;cut (U2 = NTop)
1852      [|generalize in match H5;elim U2 0;simplify;intros;destruct;reflexivity]
1853   rewrite > Hcut;apply NSA_Top;
1854      [apply (adeq_WFE2 ? H1);assumption
1855      |apply (adeq_WFT2 ? ? H2);assumption]
1856   |intros;cut (T2 = TName n ∧ U2 = TName n)
1857    [|split
1858      [generalize in match H4;elim T2 0;simplify;intros;destruct;reflexivity
1859      |generalize in match H5;elim U2 0;simplify;intros;destruct;reflexivity]]
1860    elim Hcut;
1861    rewrite > H6;rewrite > H7;apply NSA_Refl_TVar;
1862      [apply (adeq_WFE2 ? H1);assumption
1863      |rewrite > H3 in H2;rewrite < eq_fv_Nenv_fv_env in H2;assumption]
1864   |intros;cut (T2 = TName n)
1865      [|generalize in match H5;elim T2 0;simplify;intros;destruct;reflexivity]
1866    rewrite > Hcut;
1867    elim (decoder t1 O ? []);
1868      [rewrite > H4 in H1;rewrite > H7 in H1;elim (xxx ? ? ? ? H1);elim H8;
1869       apply NSA_Trans_TVar
1870         [apply a1
1871         |assumption
1872         |apply H3;autobatch]
1873      |apply (WFT_to_closed l);apply (JS_to_WFT1 ? ? ? H2)
1874      |simplify;reflexivity
1875      |unfold;intros;simplify in H7;elim (not_le_Sn_O ? H7)
1876      |apply not_in_list_nil]
1877   |intros;cut (∃u,u1,u2,u3.T2 = NArrow u u1 ∧ U2 = NArrow u2 u3)
1878      [elim Hcut;elim H8;elim H9;elim H10;elim H11;clear Hcut H8 H9 H10 H11;
1879       rewrite > H12;rewrite > H13;rewrite > H13 in H7;simplify in H7;destruct;
1880       simplify in H6;destruct;apply NSA_Arrow
1881         [apply H2;reflexivity
1882         |apply H4;reflexivity]
1883      |generalize in match H6;elim T2 0;simplify;intros;destruct;
1884       generalize in match H7;elim U2 0;simplify;intros;destruct;
1885       autobatch depth=6 width=2 size=7]
1886   |intros;cut (∃n,u,u1,n1,u2,u3.T2 = NForall n u u1 ∧ U2 = NForall n1 u2 u3)
1887      [elim Hcut;elim H8;elim H9;elim H10;elim H11;elim H12;elim H13;
1888       clear Hcut H8 H9 H10 H11 H12 H13;rewrite > H14;rewrite > H15;
1889       rewrite > H14 in H6;rewrite > H15 in H7;simplify in H6;simplify in H7;
1890       destruct H6;destruct H7;lapply (SA_All ? ? ? ? ? H1 H3);destruct H5;
1891       lapply (JS_to_WFT1 ? ? ? Hletin);lapply (JS_to_WFT2 ? ? ? Hletin);
1892       apply NSA_All
1893         [apply (adeq_WFT2 ? ? Hletin1);reflexivity
1894         |apply (adeq_WFT2 ? ? Hletin2);reflexivity
1895         |apply H2;reflexivity
1896         |intros;apply H4;
1897            [apply Z
1898            |rewrite < eq_fv_Nenv_fv_env;assumption
1899            |simplify;reflexivity
1900            |rewrite < (encode_subst a2 Z a []);
1901               [reflexivity
1902               |2,3:apply not_in_list_nil
1903               |lapply (SA_All ? ? ? ? ? H1 H3);lapply (JS_to_WFT1 ? ? ? Hletin);
1904                intro;elim (decidable_eq_nat Z a)
1905                  [assumption
1906                  |lapply (fv_WFT ? Z ? Hletin1)
1907                     [elim H5;rewrite > eq_fv_Nenv_fv_env;assumption
1908                     |simplify;apply in_list_to_in_list_append_r;
1909                      apply fv_NTyp_fv_Typ
1910                        [assumption
1911                        |intro;apply H9;autobatch]]]]
1912            |rewrite < (encode_subst a5 Z a3 [])
1913               [reflexivity
1914               |2,3:apply not_in_list_nil
1915               |intro;elim H7
1916                  [assumption
1917                  |elim (H9 H8)]]]]
1918      |generalize in match H6;elim T2 0;simplify;intros;destruct;
1919       generalize in match H7;elim U2 0;simplify;intros;destruct;
1920       autobatch depth=8 width=2 size=9]]
1921 qed.