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/defn.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,S1,S2,T1,T2.
 301               (NJSubtype G T1 S1) →
 302               (∀Y.¬(Y ∈ fv_Nenv G) →
 303               (NJSubtype ((mk_nbound true Y T1) :: G)
 304                     (swap_NTyp Y X S2) (swap_NTyp Y X T2))) →
 305               (NJSubtype G (NForall X S1 S2) (NForall X T1 T2))
 306   | NSA_alpha : ∀G,T1,T2,U1,U2.(NJSubtype G T1 U1) →
 307                                 (alpha_eq T1 T2) →
 308                                 (alpha_eq U1 U2) →
 309                                 (NJSubtype G T2 U2).
 310
 311 let rec nt_len T \def
 312   match T with
 313   [ TName X ⇒ O
 314   | NTop ⇒ O
 315   | NArrow T1 T2 ⇒ S (max (nt_len T1) (nt_len T2))
 316   | NForall X T1 T2 ⇒ S (max (nt_len T1) (nt_len T2)) ].
 317
 318 definition encodeenv : list nbound → list bound ≝
 319   map nbound bound
 320     (λb.match b with
 321        [ mk_nbound b x T ⇒ mk_bound b x (encodetype T []) ]).
 322
 323 axiom append_associative : ∀A.∀l1,l2,l3:(list A).((l1@l2)@l3) = (l1@l2@l3).
 324
 325 lemma eq_fv_Nenv_fv_env : ∀G. fv_Nenv G = fv_env (encodeenv G).
 326 intro;elim G
 327   [simplify;reflexivity
 328   |simplify;rewrite < H;elim t;simplify;reflexivity]
 329 qed.
 330
 331 (* palloso *)
 332 axiom decidable_eq_bound : \forall b,c:bound.decidable (b = c).
 333
 334 lemma in_Nenv_to_in_env: ∀l,n,n2.mk_nbound true n n2 ∈ l →
 335                  mk_bound true n (encodetype n2 []) ∈ encodeenv l.
 336 intros 3;elim l
 337   [elim (not_in_list_nil ? ? H)
 338   |inversion H1;intros
 339      [destruct H3;destruct;simplify;apply in_list_head
 340      |destruct H5;elim t;simplify;apply in_list_cons;apply H;assumption]]
 341 qed.
 342
 343 lemma in_lookup : \forall x,l.(in_list ? x l) \to (lookup x l = true).
 344 intros;elim H
 345   [simplify;rewrite > eqb_n_n;reflexivity
 346   |simplify;rewrite > H2;elim (eqb a a1);reflexivity]
 347 qed.
 348
 349 lemma lookup_in : \forall x,l.(lookup x l = true) \to (in_list ? x l).
 350 intros 2;elim l
 351   [simplify in H;destruct H
 352   |generalize in match H1;simplify;elim (decidable_eq_nat x t)
 353      [rewrite > H2;apply in_list_head
 354      |rewrite > (not_eq_to_eqb_false ? ? H2) in H3;simplify in H3;
 355       apply in_list_cons;apply H;assumption]]
 356 qed.
 357
 358 lemma posn_length : \forall x,vars.(in_list ? x vars) \to
 359                        (posn vars x) < (length ? vars).
 360 intros 2;elim vars
 361   [elim (not_in_list_nil ? ? H)
 362   |inversion H1
 363      [intros;destruct H3;destruct;simplify;rewrite > eqb_n_n;simplify;
 364       apply lt_O_S
 365      |intros;destruct H5;simplify;elim (eqb x t);simplify
 366         [apply lt_O_S
 367         |apply le_S_S;apply H;assumption]]]
 368 qed.
 369
 370 lemma in_remove : \forall a,b,l.(a \neq b) \to (in_list ? a l) \to
 371                                 (in_list ? a (remove_nat b l)).
 372 intros 4;elim l
 373   [elim (not_in_list_nil ? ? H1)
 374   |inversion H2;intros;
 375      [destruct H4;destruct;simplify;rewrite > not_eq_to_eqb_false
 376         [simplify;apply in_list_head
 377         |intro;apply H;symmetry;assumption]
 378      |destruct H6;simplify;elim (eqb b t)
 379         [simplify;apply H1;assumption
 380         |simplify;apply in_list_cons;apply H1;assumption]]]
 381 qed.
 382
 383 axiom NTyp_len_ind : \forall P:NTyp \to Prop.
 384                        (\forall U.(\forall V.((nt_len V) < (nt_len U)) \to (P V))
 385                            \to (P U))
 386                        \to \forall T.(P T).
 387
 388 axiom ntlen_arrow1 : ∀T1,T2.(nt_len T1) < (nt_len (NArrow T1 T2)).
 389 axiom ntlen_arrow2 : ∀T1,T2.(nt_len T2) < (nt_len (NArrow T1 T2)).
 390 axiom ntlen_forall1 : ∀X,T1,T2.(nt_len T1) < (nt_len (NForall X T1 T2)).
 391 axiom ntlen_forall2 : ∀X,T1,T2.(nt_len T2) < (nt_len (NForall X T1 T2)).
 392 axiom eq_ntlen_swap : ∀X,Y,T.nt_len T = nt_len (swap_NTyp X Y T).
 393
 394 axiom nat_in_list_case :\forall G:list nat
 395 .\forall H:list nat
 396  .\forall n:nat.in_list nat n (H@G)\rarr in_list nat n G\lor in_list nat n H.
 397
 398 lemma swap_same : \forall x,y.swap x x y = y.
 399 intros;elim (decidable_eq_nat y x)
 400   [autobatch paramodulation
 401   |rewrite > swap_other;autobatch]
 402 qed.
 403
 404 lemma not_nat_in_to_lookup_false : ∀l,X.¬(X ∈ l) → lookup X l = false.
 405 intros 2;elim l
 406   [simplify;reflexivity
 407   |simplify;elim (decidable_eq_nat X t)
 408      [elim H1;rewrite > H2;apply in_list_head
 409      |rewrite > (not_eq_to_eqb_false ? ? H2);simplify;apply H;intro;apply H1;
 410       apply (in_list_cons ? ? ? ? H3);]]
 411 qed.
 412
 413 lemma fv_encode : ∀T,l1,l2.
 414                   (∀x.(in_list ? x (fv_NTyp T)) →
 415                      (lookup x l1 = lookup x l2 ∧
 416                      (lookup x l1 = true → posn l1 x = posn l2 x))) →
 417                   (encodetype T l1 = encodetype T l2).
 418 intro;elim T
 419   [simplify in H;elim (H n)
 420      [simplify;rewrite < H1;generalize in match H2;elim (lookup n l1)
 421         [simplify;rewrite > H3;autobatch
 422         |simplify;reflexivity]
 423      |apply in_list_head]
 424   |simplify;reflexivity
 425   |simplify;rewrite > (H l1 l2)
 426      [rewrite > (H1 l1 l2)
 427         [reflexivity
 428         |intros;apply H2;simplify;apply in_list_to_in_list_append_r;autobatch]
 429      |intros;apply H2;simplify;apply in_list_to_in_list_append_l;autobatch]
 430   |simplify;rewrite > (H l1 l2)
 431      [rewrite > (H1 (n::l1) (n::l2))
 432         [reflexivity
 433         |intros;elim (decidable_eq_nat x n)
 434            [simplify;rewrite > (eq_to_eqb_true ? ? H4);simplify;split
 435               [reflexivity|intro;reflexivity]
 436            |elim (H2 x)
 437               [split
 438                  [simplify;rewrite < H5;reflexivity
 439                  |simplify;elim (eqb x n);
 440                     [simplify;reflexivity
 441                     |simplify in H7;rewrite < (H6 H7);reflexivity]]
 442               |simplify;apply in_list_to_in_list_append_r;
 443                apply (in_remove ? ? ? H4);assumption]]]
 444      |intros;apply H2;simplify;apply in_list_to_in_list_append_l;autobatch]]
 445 qed.
 446
 447 lemma lookup_swap : \forall a,b,x,vars.
 448                     (lookup (swap a b x) (swap_list a b vars) =
 449                     lookup x vars).
 450 intros 4;elim vars
 451   [simplify;reflexivity
 452   |simplify;elim (decidable_eq_nat x t)
 453      [rewrite > H1;rewrite > eqb_n_n;rewrite > eqb_n_n;simplify;reflexivity
 454      |rewrite > (not_eq_to_eqb_false ? ? H1);elim (decidable_eq_nat x a)
 455         [rewrite > H;rewrite > H2;rewrite > swap_left;
 456          elim (decidable_eq_nat b t)
 457            [rewrite < H3;rewrite > swap_right;
 458             rewrite > (not_eq_to_eqb_false b a)
 459               [reflexivity
 460               |intro;autobatch]
 461            |rewrite > (swap_other a b t)
 462               [rewrite > (not_eq_to_eqb_false ? ? H3);simplify;reflexivity
 463               |intro;autobatch
 464               |intro;autobatch]]
 465         |elim (decidable_eq_nat x b)
 466            [rewrite > H;rewrite > H3;rewrite > swap_right;
 467             elim (decidable_eq_nat t a)
 468               [rewrite > H4;rewrite > swap_left;
 469                rewrite > (not_eq_to_eqb_false a b)
 470                  [reflexivity
 471                  |intro;autobatch]
 472               |rewrite > (swap_other a b t)
 473                  [rewrite > (not_eq_to_eqb_false a t)
 474                     [reflexivity
 475                     |intro;autobatch]
 476                  |assumption
 477                  |intro;autobatch]]
 478            |rewrite > H;rewrite > (swap_other a b x)
 479               [elim (decidable_eq_nat a t)
 480                  [rewrite > H4;rewrite > swap_left;
 481                   rewrite > (not_eq_to_eqb_false ? ? H3);reflexivity
 482                  |elim (decidable_eq_nat b t)
 483                     [rewrite > H5;rewrite > swap_right;
 484                      rewrite > (not_eq_to_eqb_false ? ? H2);reflexivity
 485                     |rewrite > (swap_other a b t)
 486                        [rewrite > (not_eq_to_eqb_false ? ? H1);reflexivity
 487                        |intro;autobatch
 488                        |intro;autobatch]]]
 489               |assumption
 490               |assumption]]]]]
 491 qed.
 492
 493 lemma posn_swap : \forall a,b,x,vars.
 494                   (posn vars x = posn (swap_list a b vars) (swap a b x)).
 495 intros 4;elim vars
 496   [simplify;reflexivity
 497   |simplify;rewrite < H;elim (decidable_eq_nat x t)
 498      [rewrite > H1;do 2 rewrite > eqb_n_n;reflexivity
 499      |elim (decidable_eq_nat (swap a b x) (swap a b t))
 500         [elim H1;autobatch
 501         |rewrite > (not_eq_to_eqb_false ? ? H1);
 502          rewrite > (not_eq_to_eqb_false ? ? H2);reflexivity]]]
 503 qed.
 504
 505 theorem encode_swap : ∀a,x,T,vars.
 506                          ((in_list ? a (fv_NTyp T)) → (in_list ? a vars)) →
 507                          (in_list ? x vars) →
 508                       encodetype T vars =
 509                       encodetype (swap_NTyp a x T) (swap_list a x vars).
 510 intros 3;elim T
 511   [elim (decidable_eq_nat n x)
 512      [rewrite > H2;simplify in match (swap_NTyp ? ? ?);rewrite > swap_right;
 513       simplify;lapply (lookup_swap a x x vars);rewrite > swap_right in Hletin;
 514       rewrite > Hletin;cut ((in_list ? x vars) \to (lookup x vars = true))
 515         [rewrite > (Hcut H1);simplify;lapply (posn_swap a x x vars);
 516          rewrite > swap_right in Hletin1;rewrite < Hletin1;reflexivity
 517         |generalize in match x;elim vars
 518            [elim (not_in_list_nil ? ? H3)
 519            |inversion H4
 520               [intros;simplify;rewrite > eqb_n_n;reflexivity
 521               |intros;simplify;destruct H8;rewrite > (H3 ? H5);
 522                elim (eqb n1 t);reflexivity]]]
 523      |elim (decidable_eq_nat n a);
 524         [rewrite < H3;simplify;rewrite < posn_swap;rewrite > lookup_swap;
 525          rewrite < H3 in H;simplify in H;rewrite > in_lookup;
 526            [simplify;reflexivity
 527            |apply H;apply in_list_head]
 528         |simplify in ⊢ (? ? ? (? % ?));rewrite > swap_other;
 529            [apply (fv_encode ? vars (swap_list a x vars));intros;
 530             simplify in H4;cut (x1 = n)
 531               [rewrite > Hcut;elim vars
 532                  [simplify;split [reflexivity|intro;reflexivity]
 533                  |simplify;elim H5;cut
 534                     (t = a ∨t = x ∨ (t ≠ a ∧ t ≠ x))
 535                     [|elim (decidable_eq_nat t a)
 536                        [left;left;assumption
 537                        |elim (decidable_eq_nat t x)
 538                           [left;right;assumption
 539                           |right;split;assumption]]]
 540                   elim Hcut1
 541                     [elim H8
 542                        [rewrite > H9;rewrite > swap_left;
 543                         rewrite > (not_eq_to_eqb_false ? ? H2);
 544                         rewrite > (not_eq_to_eqb_false ? ? H3);simplify;
 545                         split
 546                           [assumption
 547                           |intro;rewrite < (H7 H10);reflexivity]
 548                        |rewrite > H9;rewrite > swap_right;
 549                         rewrite > (not_eq_to_eqb_false ? ? H2);
 550                         rewrite > (not_eq_to_eqb_false ? ? H3);simplify;
 551                         split
 552                           [assumption
 553                           |intro;rewrite < (H7 H10);reflexivity]]
 554                     |elim H8;rewrite > (swap_other a x t)
 555                        [rewrite < H6;split
 556                           [reflexivity
 557                           |elim (eqb n t)
 558                              [simplify;reflexivity
 559                              |simplify in H11;rewrite < (H7 H11);reflexivity]]
 560                        |*:assumption]]]
 561               |inversion H4
 562                  [intros;destruct H6;destruct;reflexivity
 563                  |intros;destruct H8;elim (not_in_list_nil ? ? H5)]]
 564            |*:assumption]]]
 565   |simplify;reflexivity
 566   |simplify;simplify in H2;rewrite < H
 567      [rewrite < H1
 568         [reflexivity
 569         |intro;apply H2;apply in_list_to_in_list_append_r;autobatch
 570         |assumption]
 571      |intro;apply H2;apply in_list_to_in_list_append_l;autobatch
 572      |assumption]
 573   |simplify;simplify in H2;rewrite < H
 574      [elim (decidable_eq_nat a n)
 575         [rewrite < (H1 (n::vars));
 576            [reflexivity
 577            |intro;rewrite > H4;apply in_list_head
 578            |apply in_list_cons;assumption]
 579         |rewrite < (H1 (n::vars));
 580            [reflexivity
 581            |intro;apply in_list_cons;apply H2;apply in_list_to_in_list_append_r;
 582             apply (in_remove ? ? ? H4 H5)
 583            |apply in_list_cons;assumption]]
 584      |intro;apply H2;apply in_list_to_in_list_append_l;assumption
 585      |assumption]]
 586 qed.
 587
 588 lemma encode_swap2 : ∀a:nat.∀x:nat.∀T:NTyp.
 589   ¬(a ∈ (fv_NTyp T)) →
 590     \forall vars.x ∈ vars
 591        →encodetype T vars=encodetype (swap_NTyp a x T) (swap_list a x vars).
 592 intros;apply (encode_swap ? ? ? ? ? H1);intro;elim (H H2);
 593 qed.
 594
 595 lemma remove_inlist : \forall x,y,l.(in_list ? x (remove_nat y l)) \to
 596                       (in_list ? x l) \land x \neq y.
 597 intros 3;elim l 0
 598   [simplify;intro;elim (not_in_list_nil ? ? H)
 599   |simplify;intro;elim (decidable_eq_nat y t)
 600      [rewrite > H in H2;rewrite > eqb_n_n in H2;simplify in H2;
 601       rewrite > H in H1;elim (H1 H2);rewrite > H;split
 602         [apply in_list_cons;assumption
 603         |assumption]
 604      |rewrite > (not_eq_to_eqb_false ? ? H) in H2;simplify in H2;
 605       inversion H2
 606         [intros;destruct H4;split
 607            [apply in_list_head
 608            |intro;autobatch]
 609         |intros;destruct H6;
 610          elim (H1 H3);split
 611            [apply in_list_cons;assumption
 612            |assumption]]]]
 613 qed.
 614
 615 lemma inlist_remove : \forall x,y,l.(in_list ? x l \to x \neq y \to
 616                 (in_list ? x (remove_nat y l))).
 617 intros 3;elim l
 618   [elim (not_in_list_nil ? ? H);
 619   |simplify;elim (decidable_eq_nat y t)
 620      [rewrite > (eq_to_eqb_true ? ? H3);simplify;apply H
 621         [(*FIXME*)generalize in match H1;intro;inversion H1
 622            [intros;destruct H6;destruct;elim H2;reflexivity
 623            |intros;destruct H8;assumption]
 624         |assumption]
 625      |rewrite > (not_eq_to_eqb_false ? ? H3);simplify;
 626       (*FIXME*)generalize in match H1;intro;inversion H4
 627         [intros;destruct H6;destruct;apply in_list_head
 628         |intros;destruct H8;destruct;apply in_list_cons;apply (H H5 H2)
 629         ]]]
 630 qed.
 631
 632 lemma incl_fv_var : \forall T.(incl ? (fv_NTyp T) (var_NTyp T)).
 633 intro;elim T
 634   [simplify;unfold;intros;assumption
 635   |simplify;unfold;intros;assumption
 636   |simplify;unfold;intros;elim (in_list_append_to_or_in_list ? ? ? ? H2)
 637      [apply in_list_to_in_list_append_l;apply (H ? H3)
 638      |apply in_list_to_in_list_append_r;apply (H1 ? H3)]
 639   |simplify;unfold;intros;elim (decidable_eq_nat x n)
 640      [rewrite > H3;apply in_list_head
 641      |apply in_list_cons;elim (in_list_append_to_or_in_list ? ? ? ? H2)
 642         [apply in_list_to_in_list_append_l;apply (H ? H4)
 643         |apply in_list_to_in_list_append_r;elim (remove_inlist ? ? ? H4);
 644          apply (H1 ? H5)]]]
 645 qed.
 646
 647 lemma fv_encode2 : ∀T,l1,l2.
 648                       (∀x.(in_list ? x (fv_NTyp T)) →
 649                            (lookup x l1 = lookup x l2 ∧
 650                             posn l1 x = posn l2 x)) →
 651                       (encodetype T l1 = encodetype T l2).
 652 intros;apply fv_encode;intros;elim (H ? H1);split
 653   [assumption|intro;assumption]
 654 qed.
 655
 656 lemma alpha_sym : \forall S,T.(alpha_eq S T) \to (alpha_eq T S).
 657 intros;elim H
 658   [apply A_refl
 659   |apply A_arrow;assumption
 660   |apply A_forall
 661      [assumption
 662      |intros;apply H4;intro;apply H5;elim (decidable_eq_nat Z n5)
 663         [rewrite > H7;apply in_list_head
 664         |apply in_list_cons;(*FIXME*)generalize in match H6;intro;
 665          inversion H6
 666            [intros;destruct H10;destruct;apply in_list_head
 667            |intros;destruct H12;apply in_list_cons;inversion H9
 668               [intros;destruct H12;elim H7;reflexivity
 669               |intros;destruct H14;
 670                elim (in_list_append_to_or_in_list ? ? ? ? H11)
 671                  [apply in_list_to_in_list_append_r;assumption
 672                  |apply in_list_to_in_list_append_l;assumption]]]]]]
 673 qed.
 674
 675 lemma inlist_fv_swap : \forall x,y,b,T.
 676                    (\lnot (in_list ? b (y::var_NTyp T))) \to
 677                    (in_list ? x (fv_NTyp (swap_NTyp b y T))) \to
 678                    (x \neq y \land (x = b \lor (in_list ? x (fv_NTyp T)))).
 679 intros 4;elim T
 680   [simplify in H;simplify;simplify in H1;elim (decidable_eq_nat y n)
 681      [rewrite > H2 in H1;rewrite > swap_right in H1;
 682       inversion H1
 683         [intros;destruct H4;split
 684            [unfold;intro;apply H;rewrite > H2;apply in_list_head
 685            |left;reflexivity]
 686         |intros;destruct H6;elim (not_in_list_nil ? ? H3)]
 687      |elim (decidable_eq_nat b n)
 688         [rewrite > H3 in H;elim H;apply in_list_cons;apply in_list_head
 689         |rewrite > swap_other in H1
 690            [split
 691               [inversion H1
 692                  [intros;destruct H5;intro;apply H2;
 693                   symmetry;assumption
 694                  |intros;destruct H7;
 695                   elim (not_in_list_nil ? ? H4)]
 696               |autobatch]
 697            |intro;autobatch
 698            |intro;autobatch]]]
 699   |simplify in H1;elim (not_in_list_nil ? ? H1)
 700   |simplify;simplify in H3;simplify in H2;elim (nat_in_list_case ? ? ? H3)
 701      [elim H1
 702         [split
 703            [assumption
 704            |elim H6
 705               [left;assumption
 706               |right;apply in_list_to_in_list_append_r;assumption]]
 707            |intro;apply H2;elim (nat_in_list_case (var_NTyp n1) [y] ? H5)
 708               [apply (in_list_to_in_list_append_r ? ? (y::var_NTyp n) (var_NTyp n1));
 709                assumption
 710               |inversion H6
 711                  [intros;destruct H8;apply in_list_head
 712                  |intros;destruct H10;
 713                   elim (not_in_list_nil ? ? H7)]]
 714            |assumption]
 715         |elim H
 716            [split
 717               [assumption
 718               |elim H6
 719                  [left;assumption
 720                  |right;apply in_list_to_in_list_append_l;assumption]]
 721            |intro;apply H2;inversion H5
 722               [intros;destruct H7;apply in_list_head
 723               |intros;destruct H9;apply in_list_cons;
 724                apply in_list_to_in_list_append_l;assumption]
 725            |assumption]]
 726    |simplify;simplify in H3;simplify in H2;elim (nat_in_list_case ? ? ? H3)
 727       [elim H1
 728          [split
 729             [assumption
 730             |elim H6
 731                [left;assumption
 732                |right;apply in_list_to_in_list_append_r;apply inlist_remove
 733                   [assumption
 734                   |intro;elim (remove_inlist ? ? ? H4);apply H10;
 735                    rewrite > swap_other
 736                      [assumption
 737                      |intro;rewrite > H8 in H7;rewrite > H11 in H7;apply H2;
 738                       destruct;apply in_list_cons;apply in_list_head
 739                      |destruct;assumption]]]]
 740          |intro;apply H2;inversion H5
 741             [intros;destruct H7;apply in_list_head
 742             |intros;destruct H9;
 743              apply in_list_cons;
 744              cut ((n::var_NTyp n1)@(var_NTyp n2) = n::var_NTyp n1@var_NTyp n2)
 745                [rewrite < Hcut;elim (n::var_NTyp n1)
 746                   [simplify;assumption
 747                   |simplify;elim (decidable_eq_nat b t)
 748                      [rewrite > H9;apply in_list_head
 749                      |apply in_list_cons;assumption]]
 750                |simplify;reflexivity]]
 751          |elim(remove_inlist ? ? ? H4);assumption]
 752       |elim H
 753          [split
 754             [assumption
 755             |elim H6
 756                [left;assumption
 757                   |right;apply in_list_to_in_list_append_l;
 758                    assumption]]
 759             |intro;apply H2;inversion H5
 760                [intros;destruct H7;apply in_list_head
 761                |intros;destruct H9;apply in_list_cons;
 762                 elim (decidable_eq_nat b n)
 763                   [rewrite > H8;apply in_list_head
 764                   |apply in_list_cons;apply in_list_to_in_list_append_l;
 765                    assumption]]
 766             |assumption]]]
 767 qed.
 768
 769 lemma inlist_fv_swap_r : \forall x,y,b,T.
 770                    (\lnot (in_list ? b (y::var_NTyp T))) \to
 771                    ((x = b \land (in_list ? y (fv_NTyp T))) \lor
 772                     (x \neq y \land (in_list ? x (fv_NTyp T)))) \to
 773                    (in_list ? x (fv_NTyp (swap_NTyp b y T))).
 774 intros 4;elim T
 775   [simplify;simplify in H;simplify in H1;cut (b \neq n)
 776      [elim H1
 777         [elim H2;cut (y = n)
 778            [rewrite > Hcut1;rewrite > swap_right;rewrite > H3;apply in_list_head
 779            |inversion H4
 780               [intros;destruct H6;autobatch
 781               |intros;destruct H8;elim (not_in_list_nil ? ? H5)]]
 782         |elim H2;inversion H4
 783            [intros;destruct H6;destruct;rewrite > (swap_other b y x)
 784               [apply in_list_head
 785               |intro;autobatch
 786               |assumption]
 787            |intros;destruct H8;elim (not_in_list_nil ? ? H5)]]
 788         |intro;apply H;apply (in_list_to_in_list_append_r ? ? [y] [n]);
 789          rewrite > H2;apply in_list_head]
 790   |simplify in H1;elim H1;elim H2;elim (not_in_list_nil ? ? H4)
 791   |simplify;simplify in H3;cut (\lnot (in_list ? b (y::var_NTyp n1)))
 792      [cut (\lnot (in_list ? b (y::var_NTyp n)))
 793         [elim H3
 794            [elim H4;elim (in_list_append_to_or_in_list ? ? ? ? H6)
 795               [apply in_list_to_in_list_append_l;apply H
 796                  [assumption
 797                  |left;split;assumption]
 798               |apply in_list_to_in_list_append_r;apply H1
 799                  [assumption
 800                  |left;split;assumption]]
 801            |elim H4;elim (in_list_append_to_or_in_list ? ? ? ? H6)
 802               [apply in_list_to_in_list_append_l;apply H;
 803                  [assumption
 804                  |right;split;assumption]
 805               |apply in_list_to_in_list_append_r;apply H1
 806                  [assumption
 807                  |right;split;assumption]]]
 808         |intro;apply H2;inversion H4
 809            [intros;destruct H6;apply in_list_head
 810            |intros;destruct H8;apply in_list_cons;
 811             simplify;apply in_list_to_in_list_append_l;
 812             assumption]]
 813      |intro;apply H2;inversion H4
 814         [intros;destruct H6;apply in_list_head
 815         |intros;destruct H8;apply in_list_cons;
 816          simplify;apply in_list_to_in_list_append_r;
 817          assumption]]
 818   |simplify;simplify in H3;cut (\lnot (in_list ? b (y::var_NTyp n1)))
 819      [cut (\lnot (in_list ? b (y::var_NTyp n2)))
 820         [elim H3
 821            [elim H4;elim (in_list_append_to_or_in_list ? ? ? ? H6)
 822               [apply in_list_to_in_list_append_l;apply H
 823                  [assumption
 824                  |left;split;assumption]
 825               |apply in_list_to_in_list_append_r;apply inlist_remove
 826                  [apply H1;
 827                     [assumption
 828                     |left;split
 829                        [assumption|elim (remove_inlist ? ? ? H7);assumption]]
 830                  |elim (remove_inlist ? ? ? H7);elim (decidable_eq_nat b n)
 831                     [rewrite > H10;rewrite > swap_left;intro;apply H9;
 832                      rewrite < H11;rewrite < H10;assumption
 833                     |rewrite > swap_other
 834                        [rewrite > H5;assumption
 835                        |intro;apply H10;symmetry;assumption
 836                        |intro;apply H9;symmetry;assumption]]]]
 837            |elim H4;elim (in_list_append_to_or_in_list ? ? ? ? H6)
 838               [apply in_list_to_in_list_append_l;apply H
 839                  [assumption
 840                  |right;split;assumption]
 841               |apply in_list_to_in_list_append_r;apply inlist_remove
 842                  [apply H1;
 843                     [assumption
 844                     |right;split
 845                        [assumption|elim (remove_inlist ? ? ? H7);assumption]]
 846                  |elim (decidable_eq_nat b n)
 847                     [rewrite > H8;rewrite > swap_left;assumption
 848                     |elim (decidable_eq_nat y n)
 849                        [rewrite > H9;rewrite > swap_right;intro;apply Hcut1;
 850                         rewrite > H9;apply in_list_cons;
 851                         apply incl_fv_var;elim (remove_inlist ? ? ? H7);
 852                         rewrite < H10;assumption
 853                        |rewrite > (swap_other b y n)
 854                           [elim (remove_inlist ? ? ? H7);assumption
 855                           |intro;autobatch
 856                           |intro;autobatch]]]]]]
 857         |intro;apply H2;inversion H4
 858            [intros;destruct H6;apply in_list_head
 859            |simplify;intros;destruct H8;
 860             apply in_list_cons;
 861             apply (in_list_to_in_list_append_r ? ? (n::var_NTyp n1) (var_NTyp n2));
 862             assumption]]
 863      |intro;apply H2;inversion H4
 864         [intros;destruct H6;apply in_list_head
 865         |simplify;intros;destruct H8;
 866          apply in_list_cons;
 867          apply (in_list_to_in_list_append_l ? ? (n::var_NTyp n1) (var_NTyp n2));
 868          apply in_list_cons;assumption]]]
 869 qed.
 870
 871 lemma fv_alpha : \forall S,T.(alpha_eq S T) \to
 872                  (incl ? (fv_NTyp S) (fv_NTyp T)).
 873 intros;elim H
 874   [unfold;intros;assumption
 875   |simplify;unfold;intros;elim (in_list_append_to_or_in_list ? ? ? ? H5)
 876      [apply in_list_to_in_list_append_l;autobatch
 877      |apply in_list_to_in_list_append_r;autobatch]
 878   |simplify;unfold;intros;
 879    elim (in_list_append_to_or_in_list ? ? ? ? H5)
 880      [apply in_list_to_in_list_append_l;apply (H2 ? H6)
 881      |elim (fresh_name (n4::n5::var_NTyp n1@var_NTyp n3));
 882       apply in_list_to_in_list_append_r;
 883       lapply (H4 ? H7);
 884       elim (remove_inlist ? ? ? H6);apply inlist_remove
 885         [lapply (inlist_fv_swap_r x n4 a n1)
 886            [elim (inlist_fv_swap x n5 a n3)
 887               [elim H11
 888                  [rewrite < H12 in H7;elim H7;
 889                   do 2 apply in_list_cons;
 890                   apply in_list_to_in_list_append_l;
 891                   apply (incl_fv_var n1 ? H8);
 892                  |assumption]
 893               |intro;apply H7;inversion H10;intros;destruct;
 894                  [apply in_list_cons;apply in_list_head
 895                  |do 2 apply in_list_cons;apply in_list_to_in_list_append_r;
 896                   assumption]
 897               |apply (Hletin ? Hletin1)]
 898            |intro;apply H7;inversion H10
 899               [intros;destruct H12;apply in_list_head
 900               |intros;destruct H14;do 2 apply in_list_cons;
 901                apply in_list_to_in_list_append_l;assumption]
 902            |right;split;assumption]
 903         |intros;intro;lapply (inlist_fv_swap_r x n4 a n1)
 904            [lapply (Hletin ? Hletin1);
 905             elim (inlist_fv_swap x n5 a n3 ? Hletin2)
 906               [apply (H11 H10)
 907               |intro;apply H7;elim (decidable_eq_nat a n4)
 908                  [rewrite > H12;apply in_list_head
 909                  |apply in_list_cons;inversion H11;intros;destruct;
 910                     [apply in_list_head
 911                     |apply in_list_cons;apply in_list_to_in_list_append_r;
 912                      assumption]]]
 913            |intro;apply H7;inversion H11
 914               [intros;destruct H13;apply in_list_head
 915               |intros;destruct H15;do 2 apply in_list_cons;
 916                apply in_list_to_in_list_append_l;assumption]
 917            |right;split;assumption]]]]
 918 qed.
 919
 920 theorem alpha_to_encode : ∀S,T.(alpha_eq S T) →
 921                              ∀vars.(encodetype S vars) = (encodetype T vars).
 922 intros 3;elim H
 923   [reflexivity
 924   |simplify;rewrite > H2;rewrite > H4;reflexivity
 925   |simplify;rewrite > H2;
 926    cut (encodetype n1 (n4::vars) = encodetype n3 (n5::vars))
 927      [rewrite > Hcut;reflexivity
 928      |elim (fresh_name (n4::n5::var_NTyp n1@var_NTyp n3));
 929       lapply (encode_swap2 a n4 n1 ? (n4::vars))
 930         [intro;apply H5;do 2 apply in_list_cons;
 931          apply in_list_to_in_list_append_l;autobatch
 932         |lapply (encode_swap2 a n5 n3 ? (n5::vars))
 933            [intro;apply H5;do 2 apply in_list_cons;
 934             apply in_list_to_in_list_append_r;autobatch
 935            |rewrite > Hletin;rewrite > Hletin1;simplify;rewrite > swap_right;
 936             rewrite > swap_right;rewrite > (H4 a H5 (a::swap_list a n4 vars));
 937             rewrite > (fv_encode2 ? ? (a::swap_list a n5 vars))
 938               [reflexivity
 939               |intros;elim (decidable_eq_nat n4 n5)
 940                  [rewrite > H7;autobatch
 941                  |cut ((x \neq n4) \land (x \neq n5))
 942                     [elim Hcut;elim (decidable_eq_nat x a)
 943                        [simplify;rewrite > (eq_to_eqb_true ? ? H10);simplify;
 944                         autobatch
 945                        |simplify;rewrite > (not_eq_to_eqb_false ? ? H10);
 946                         simplify;elim vars
 947                              [simplify;autobatch
 948                              |simplify;elim H11;rewrite < H12;
 949                               rewrite > H13;elim (decidable_eq_nat a t)
 950                                 [rewrite > H14;rewrite > swap_left;
 951                                  rewrite > swap_left;
 952                                  rewrite > (not_eq_to_eqb_false ? ? H8);
 953                                  rewrite > (not_eq_to_eqb_false ? ? H9);
 954                                  simplify;autobatch
 955                                 |elim (decidable_eq_nat n4 t)
 956                                    [rewrite > H15;rewrite > swap_right;
 957                                     rewrite > (swap_other a n5 t)
 958                                        [rewrite > (not_eq_to_eqb_false ? ? H10);
 959                                         rewrite < H15;
 960                                         rewrite > (not_eq_to_eqb_false ? ? H8);
 961                                         autobatch
 962                                        |intro;autobatch
 963                                        |intro;apply H7;autobatch]
 964                                    |rewrite > (swap_other a n4 t);
 965                                     elim (decidable_eq_nat n5 t)
 966                                       [rewrite < H16;rewrite > swap_right;
 967                                     rewrite > (not_eq_to_eqb_false ? ? H9);
 968                                     rewrite > (not_eq_to_eqb_false ? ? H10);
 969                                     autobatch
 970                                    |rewrite > (swap_other a n5 t);try intro;
 971                                     autobatch
 972                                    |*:intro;autobatch]]]]]
 973                        |split
 974                           [lapply (H3 ? H5);lapply (alpha_sym ? ? Hletin2);
 975                            lapply (fv_alpha ? ? Hletin3);
 976                            lapply (Hletin4 ? H6);
 977                            elim (inlist_fv_swap ? ? ? ? ? Hletin5)
 978                              [assumption
 979                              |intro;apply H5;inversion H8
 980                                 [intros;destruct H10;
 981                                  apply in_list_head
 982                                 |intros;destruct H12;
 983                                  do 2 apply in_list_cons;
 984                                  apply in_list_to_in_list_append_l;assumption]]
 985                           |elim (inlist_fv_swap ? ? ? ? ? H6)
 986                              [assumption
 987                              |intro;apply H5;elim (decidable_eq_nat a n4)
 988                                 [rewrite > H9;apply in_list_head
 989                                 |apply in_list_cons;
 990                                  inversion H8;intros;destruct;
 991                                    [apply in_list_head
 992                                    |apply in_list_cons;
 993                                     apply in_list_to_in_list_append_r;
 994                                     assumption]]]]]]]
 995               |apply in_list_head]
 996            |apply in_list_head]]]
 997 qed.
 998
 999 lemma encode_append : ∀T,U,n,l.length ? l ≤ n →
1000         subst_type_nat (encodetype T l) U n = encodetype T l.
1001 intros 2;elim T
1002   [simplify;elim (bool_to_decidable_eq (lookup n l) true)
1003      [rewrite > H1;simplify;lapply (lookup_in ? ? H1);
1004       lapply (posn_length ? ? Hletin);
1005       cut (posn l n ≠ n1)
1006         [rewrite > (not_eq_to_eqb_false ? ? Hcut);simplify;reflexivity
1007         |intro;rewrite > H2 in Hletin1;unfold in Hletin1;autobatch;]
1008      |cut (lookup n l = false)
1009         [rewrite > Hcut;reflexivity
1010         |generalize in match H1;elim (lookup n l);
1011            [elim H2;reflexivity|reflexivity]]]
1012   |simplify;reflexivity
1013   |simplify;autobatch
1014   |simplify;rewrite > (H ? ? H2);rewrite > H1
1015      [reflexivity
1016      |simplify;autobatch]]
1017 qed.
1018
1019 lemma encode_subst_simple : ∀X,T,l.
1020      (encodetype T l = subst_type_nat (encodetype T (l@[X])) (TFree X) (length ? l)).
1021 intros 2;elim T
1022   [simplify;cut (lookup n l = true → posn l n = posn (l@[X]) n)
1023      [generalize in match Hcut;elim (bool_to_decidable_eq (lookup n l) true)
1024         [cut (lookup n (l@[X]) = true)
1025            [rewrite > H;rewrite > Hcut1;simplify;
1026             cut (eqb (posn (l@[X]) n) (length nat l) = false)
1027               [rewrite > Hcut2;simplify;rewrite < (H1 H);reflexivity
1028               |generalize in match H;elim l 0
1029                  [simplify;intro;destruct H2
1030                  |intros 2;simplify;elim (eqb n t)
1031                     [simplify;reflexivity
1032                     |simplify in H3;simplify;apply (H2 H3)]]]
1033            |generalize in match H;elim l
1034               [simplify in H2;destruct H2
1035               |generalize in match H3;simplify;elim (eqb n t) 0
1036                  [simplify;intro;reflexivity
1037                  |simplify;intro;apply (H2 H4)]]]
1038         |cut (lookup n l = false)
1039            [elim (decidable_eq_nat n X)
1040               [rewrite > Hcut1;rewrite > H2;cut (lookup X (l@[X]) = true)
1041                  [rewrite > Hcut2;simplify;
1042                   cut (eqb (posn (l@[X]) X) (length nat l) = true)
1043                     [rewrite > Hcut3;simplify;reflexivity
1044                     |generalize in match Hcut1;elim l 0
1045                        [intros;simplify;rewrite > eqb_n_n;simplify;reflexivity
1046                        |simplify;intros 2;rewrite > H2;elim (eqb X t)
1047                           [simplify in H4;destruct H4
1048                           |simplify;simplify in H4;apply (H3 H4)]]]
1049                  |elim l
1050                     [simplify;rewrite > eqb_n_n;reflexivity
1051                     |simplify;elim (eqb X t)
1052                        [simplify;reflexivity
1053                        |simplify;assumption]]]
1054               |cut (lookup n l = lookup n (l@[X]))
1055                  [rewrite < Hcut2;rewrite > Hcut1;simplify;reflexivity
1056                  |elim l
1057                     [simplify;rewrite > (not_eq_to_eqb_false ? ? H2);simplify;
1058                      reflexivity
1059                     |simplify;elim (eqb n t)
1060                        [simplify;reflexivity
1061                        |simplify;assumption]]]]
1062            |generalize in match H;elim (lookup n l);
1063               [elim H2;reflexivity|reflexivity]]]
1064      |elim l 0
1065         [intro;simplify in H;destruct H
1066         |simplify;intros 2;elim (eqb n t)
1067            [simplify;reflexivity
1068            |simplify in H1;simplify;rewrite < (H H1);reflexivity]]]
1069   |simplify;reflexivity
1070   |simplify;rewrite < H;rewrite < H1;reflexivity
1071   |simplify;rewrite < H;rewrite < (append_associative ? [n] l [X]);
1072    rewrite < (H1 ([n]@l));reflexivity]
1073 qed.
1074
1075 lemma encode_subst : ∀T,X,Y,l.¬(X ∈ l) → ¬(Y ∈ l) →
1076                               (X ∈ (fv_NTyp T) → X = Y) →
1077                               encodetype (swap_NTyp X Y T) l =
1078                  subst_type_nat (encodetype T (l@[Y])) (TFree X) (length ? l).
1079 apply NTyp_len_ind;intro;elim U
1080   [elim (decidable_eq_nat n X)
1081      [rewrite > H4 in H3;rewrite > H4;rewrite > H3
1082         [simplify in \vdash (? ? (? % ?) ?);rewrite > swap_same;
1083          cut (lookup Y (l@[Y]) = true)
1084            [simplify;rewrite > Hcut;rewrite > (not_nat_in_to_lookup_false ? ? H2);
1085             simplify;cut (posn (l@[Y]) Y = length ? l)
1086               [rewrite > Hcut1;rewrite > eqb_n_n;reflexivity
1087               |generalize in match H2;elim l;simplify
1088                  [rewrite > eqb_n_n;reflexivity
1089                  |elim (decidable_eq_nat Y t)
1090                     [elim H6;rewrite > H7;apply in_list_head
1091                     |rewrite > (not_eq_to_eqb_false ? ? H7);simplify;
1092                      rewrite < H5
1093                        [reflexivity
1094                        |intro;apply H6;apply in_list_cons;assumption]]]]
1095            |elim l
1096               [simplify;rewrite > eqb_n_n;reflexivity
1097               |simplify;rewrite > H5;elim (eqb Y t);reflexivity]]
1098         |simplify;apply in_list_head]
1099      |elim (decidable_eq_nat Y n);
1100         [rewrite < H5;simplify;rewrite > swap_right;
1101          rewrite > (not_nat_in_to_lookup_false ? ? H1);
1102          cut (lookup Y (l@[Y]) = true)
1103            [rewrite > Hcut;simplify;cut (posn (l@[Y]) Y = length ? l)
1104               [rewrite > Hcut1;rewrite > eqb_n_n;reflexivity
1105               |generalize in match H2;elim l;simplify
1106                  [rewrite > eqb_n_n;reflexivity
1107                  |elim (decidable_eq_nat Y t)
1108                     [elim H7;rewrite > H8;apply in_list_head
1109                     |rewrite > (not_eq_to_eqb_false ? ? H8);simplify;
1110                      rewrite < H6
1111                        [reflexivity
1112                        |intro;apply H7;apply in_list_cons;assumption]]]]
1113            |elim l;simplify
1114                  [rewrite > eqb_n_n;reflexivity
1115                  |elim (eqb Y t);simplify;autobatch]]
1116         |simplify;rewrite > (swap_other X Y n)
1117            [cut (lookup n l = lookup n (l@[Y]) ∧
1118                  (lookup n l = true → posn l n = posn (l@[Y]) n))
1119               [elim Hcut;rewrite > H6;generalize in match H7;
1120                generalize in match H6;elim (lookup n (l@[Y]))
1121                  [simplify;rewrite < H9;generalize in match H8;elim l
1122                     [simplify in H10;destruct H10
1123                     |elim (decidable_eq_nat n t)
1124                        [simplify;rewrite > (eq_to_eqb_true ? ? H12);simplify;
1125                         reflexivity
1126                        |simplify;rewrite > (not_eq_to_eqb_false ? ? H12);
1127                         simplify;generalize in match H10;
1128                         elim (eqb (posn l1 n) (length nat l1))
1129                           [simplify in H13;simplify in H11;
1130                            rewrite > (not_eq_to_eqb_false ? ? H12) in H11;
1131                            simplify in H11;lapply (H13 H11);destruct Hletin
1132                           |simplify;reflexivity]]
1133                     |assumption
1134                     |assumption]
1135                  |simplify;reflexivity]
1136               |elim l;split
1137                  [simplify;cut (n ≠ Y)
1138                     [rewrite > (not_eq_to_eqb_false ? ? Hcut);simplify;
1139                      reflexivity
1140                     |intro;apply H5;symmetry;assumption]
1141                  |intro;simplify in H6;destruct H6
1142                  |elim H6;simplify;rewrite < H7;reflexivity
1143                  |simplify;elim (eqb n t)
1144                     [simplify;reflexivity
1145                     |simplify;simplify in H7;elim H6;rewrite < (H9 H7);
1146                      reflexivity]]]
1147            |assumption
1148            |intro;apply H5;symmetry;assumption]]]
1149   |simplify;reflexivity
1150   |simplify;rewrite < (H2 n ? ? ? ? H3 H4)
1151      [rewrite < (H2 n1 ? ? ? ? H3 H4);
1152         [autobatch|autobatch
1153         |intro;apply H5;simplify;apply in_list_to_in_list_append_r;assumption]
1154      |autobatch
1155      |intro;apply H5;simplify;apply in_list_to_in_list_append_l;assumption]
1156   |simplify;rewrite < (H2 n1 ? ? ? ? H3 H4)
1157      [cut (l = swap_list X Y l)
1158            [|generalize in match H3;generalize in match H4;elim l
1159                [simplify;reflexivity
1160                |simplify;elim (decidable_eq_nat t X)
1161                   [elim H8;rewrite > H9;apply in_list_head
1162                   |elim (decidable_eq_nat t Y)
1163                      [elim H7;rewrite > H10;apply in_list_head
1164                      |rewrite > (swap_other X Y t)
1165                         [rewrite < H6
1166                            [reflexivity
1167                            |intro;apply H7;apply in_list_cons;assumption
1168                            |intro;apply H8;apply in_list_cons;assumption]
1169                         |*:assumption]]]]]
1170       elim (decidable_eq_nat n Y)
1171         [rewrite > H6;rewrite > (fv_encode (swap_NTyp X Y n2) (swap X Y Y::l)
1172                       (swap_list X Y (Y::l)));
1173            [rewrite < (encode_swap X Y n2);
1174               [rewrite < (fv_encode ? (Y::l) (Y::l@[Y]))
1175                  [rewrite > encode_append;
1176                     [rewrite < (fv_encode n2 (Y::l) (Y::l@[Y]));
1177                        [reflexivity
1178                        |intros;elim (decidable_eq_nat x Y)
1179                           [rewrite > H8;simplify;rewrite > eqb_n_n;simplify;
1180                            split [reflexivity|intro;reflexivity]
1181                           |simplify;rewrite > (not_eq_to_eqb_false ? ? H8);
1182                            simplify;elim l
1183                              [simplify;rewrite > (not_eq_to_eqb_false ? ? H8);
1184                               simplify;split [reflexivity|intro;destruct H9]
1185                              |elim H9;simplify;elim (eqb x t)
1186                                 [simplify;split [reflexivity|intro;reflexivity]
1187                                 |simplify;rewrite < H10;generalize in match H11;
1188                                  elim (lookup x l1)
1189                                    [split
1190                                       [reflexivity
1191                                       |intro;rewrite < (H12 H13);reflexivity]
1192                                    |split [reflexivity|intro;destruct H13]]]]]]
1193                     |simplify;constructor 1]
1194                  |intros;simplify;elim (decidable_eq_nat x Y)
1195                     [rewrite > (eq_to_eqb_true ? ? H8);simplify;split
1196                        [reflexivity|intro;reflexivity]
1197                     |rewrite > (not_eq_to_eqb_false ? ? H8);simplify;elim l
1198                        [simplify;rewrite > (not_eq_to_eqb_false ? ? H8);
1199                         simplify;split [reflexivity|intro;destruct H9]
1200                        |simplify;elim (eqb x t)
1201                           [simplify;split [reflexivity|intro;reflexivity]
1202                           |simplify;elim H9;split
1203                              [assumption
1204                              |intro;rewrite < (H11 H12);reflexivity]]]]]
1205               |intro;elim (decidable_eq_nat X Y)
1206                  [rewrite > H8;apply in_list_head
1207                  |elim H8;apply H5;simplify;apply in_list_to_in_list_append_r;
1208                   rewrite > H6;apply (in_remove ? ? ? H8 H7)]
1209               |apply in_list_head]
1210            |intros;simplify;rewrite > swap_right;rewrite < Hcut;
1211             split [reflexivity|intro;reflexivity]]
1212         |rewrite < Hcut;elim (decidable_eq_nat n X)
1213            [rewrite > H7;rewrite > (fv_encode (swap_NTyp X Y n2) (swap X Y X::l)
1214                          (swap_list X Y (X::l)))
1215               [rewrite > (encode_swap X Y n2);
1216                  [simplify;
1217                   cut (swap X Y X::swap_list X Y (l@[Y]) =
1218                         (swap X Y X::swap_list X Y l)@[X])
1219                     [rewrite > Hcut1;cut (S (length ? l) = (length ? (swap X Y X::swap_list X Y l)))
1220                        [rewrite > Hcut2;rewrite < (encode_subst_simple X
1221                               (swap_NTyp X Y n2) (swap X Y X::swap_list X Y l));
1222                         reflexivity
1223                        |simplify;elim l
1224                           [reflexivity
1225                           |simplify;rewrite < H8;reflexivity]]
1226                     |simplify;elim l
1227                        [simplify;rewrite > swap_right;reflexivity
1228                        |simplify;destruct H8;rewrite > Hcut1;reflexivity]]
1229                  |intro;apply in_list_head
1230                  |apply in_list_cons;elim l
1231                     [simplify;apply in_list_head
1232                     |simplify;apply in_list_cons;assumption]]
1233               |intros;simplify;rewrite < Hcut;
1234                split [reflexivity|intro;reflexivity]]
1235            |rewrite > (swap_other X Y n)
1236               [rewrite < (append_associative ? [n] l [Y]);
1237                cut (S (length nat l) = length nat (n::l)) [|reflexivity]
1238                rewrite > Hcut1;rewrite < (H2 n2);
1239                  [reflexivity
1240                  |autobatch
1241                  |intro;apply H7;inversion H8;intros
1242                     [destruct H10;reflexivity
1243                     |destruct H12;destruct;elim (H3 H9)]
1244                  |intro;apply H6;inversion H8;intros
1245                     [destruct H10;reflexivity
1246                     |destruct H12;destruct;elim (H4 H9)]
1247                  |intro;apply H5;simplify;apply in_list_to_in_list_append_r;
1248                   apply (in_remove ? ? ? ? H8);intro;apply H7;symmetry;assumption]
1249               |*:assumption]]]
1250      |autobatch
1251      |intro;apply H5;simplify;apply in_list_to_in_list_append_l;assumption]]
1252 qed.
1253
1254 lemma swap_case: ∀u,v,x.(swap u v x) = u ∨ (swap u v x) = v ∨ (swap u v x = x).
1255 intros.unfold in match swap.simplify.elim (eqb x u)
1256   [simplify;autobatch
1257   |simplify;elim (eqb x v);simplify;autobatch]
1258 qed.
1259
1260 lemma in_fvNTyp_in_fvNenv : ∀G,T.(NWFType G T) → (incl ? (fv_NTyp T) (fv_Nenv G)).
1261 intros;elim H
1262   [simplify;unfold;intros;inversion H2;intros
1263      [destruct H4;assumption
1264      |destruct H6;elim (not_in_list_nil ? ? H3)]
1265   |simplify;unfold;intros;elim (not_in_list_nil ? ? H1)
1266   |simplify;unfold;intros;elim (in_list_append_to_or_in_list ? ? ? ? H5)
1267      [apply (H2 ? H6)|apply (H4 ? H6)]
1268   |simplify;unfold;intros;elim (in_list_append_to_or_in_list ? ? ? ? H5)
1269      [apply H2;assumption
1270      |elim (fresh_name (x::fv_Nenv l@var_NTyp n2));lapply (H4 a)
1271         [cut (a ≠ x ∧ x ≠ n)
1272            [elim Hcut;lapply (Hletin x)
1273               [simplify in Hletin1;inversion Hletin1;intros;
1274                  [destruct H11;elim H8;reflexivity
1275                  |destruct H13;assumption]
1276               |generalize in match H6;generalize in match H7;elim n2
1277                  [simplify in H11;elim (decidable_eq_nat n n3)
1278                     [rewrite > (eq_to_eqb_true ? ? H12) in H11;simplify in H11;
1279                      elim (not_in_list_nil ? ? H11)
1280                     |rewrite > (not_eq_to_eqb_false ? ? H12) in H11;
1281                      simplify in H11;inversion H11;intros
1282                        [destruct H14;simplify;
1283                         rewrite > swap_other
1284                           [apply in_list_head
1285                           |intro;apply H8;rewrite > H13;reflexivity
1286                           |intro;apply H9;rewrite > H13;reflexivity]
1287                        |destruct H16;elim (not_in_list_nil ? ? H13)]]
1288                  |simplify in H11;elim (not_in_list_nil ? ? H11)
1289                  |simplify in H13;simplify;elim (remove_inlist ? ? ? H13);
1290                   elim (in_list_append_to_or_in_list ? ? ? ? H14)
1291                     [apply in_list_to_in_list_append_l;apply H10
1292                        [rewrite < (append_associative ? [x] (fv_Nenv l) (var_NTyp n4));
1293                         intro;apply H12;simplify;
1294                         rewrite < (append_associative ? [x] (fv_Nenv l) (var_NTyp n3 @ var_NTyp n4));
1295                         elim (in_list_append_to_or_in_list ? ? (x::fv_Nenv l) (var_NTyp n3) H17);
1296                           [apply in_list_to_in_list_append_l;assumption
1297                           |apply in_list_to_in_list_append_r;
1298                            apply in_list_to_in_list_append_l;assumption]
1299                        |apply (in_remove ? ? ? H15 H16)]
1300                     |apply in_list_to_in_list_append_r;apply H11
1301                        [rewrite < (append_associative ? [x] (fv_Nenv l) (var_NTyp n3));
1302                         intro;apply H12;simplify;
1303                         rewrite < (append_associative ? [x] (fv_Nenv l) (var_NTyp n3 @ var_NTyp n4));
1304                         elim (in_list_append_to_or_in_list ? ? (x::fv_Nenv l) (var_NTyp n4) H17);
1305                           [apply in_list_to_in_list_append_l;assumption
1306                           |apply in_list_to_in_list_append_r;
1307                            apply in_list_to_in_list_append_r;assumption]
1308                        |apply (in_remove ? ? ? H15 H16)]]
1309                  |simplify;simplify in H13;elim (remove_inlist ? ? ? H13);
1310                   elim (nat_in_list_case ? ? ? H14);
1311                     [apply in_list_to_in_list_append_r;apply in_remove;
1312                        [elim (remove_inlist ? ? ? H16);intro;apply H18;
1313                         elim (swap_case a n n3)
1314                           [elim H20
1315                              [elim H8;symmetry;rewrite < H21;assumption
1316                              |elim H9;rewrite < H21;assumption]
1317                           |rewrite < H20;assumption]
1318                        |apply H11;
1319                           [rewrite < (append_associative ? [x] (fv_Nenv l) (var_NTyp n5));
1320                            intro;apply H12;simplify;
1321                            rewrite < (append_associative ? [x] (fv_Nenv l) (n3::var_NTyp n4 @ var_NTyp n5));
1322                            elim (nat_in_list_case ? ? ? H17)
1323                              [apply in_list_to_in_list_append_r;
1324                               apply in_list_cons;
1325                               apply in_list_to_in_list_append_r;assumption
1326                              |apply in_list_to_in_list_append_l;assumption]
1327                           |elim (remove_inlist ? ? ? H16);apply in_remove
1328                              [assumption
1329                              |assumption]]]
1330                     |apply in_list_to_in_list_append_l;apply H10;
1331                        [rewrite < (append_associative ? [x] (fv_Nenv l) (var_NTyp n4));
1332                         intro;apply H12;simplify;
1333                         rewrite < (append_associative ? [x] (fv_Nenv l) (n3::var_NTyp n4@var_NTyp n5));
1334                         elim (nat_in_list_case ? ? ? H17)
1335                           [apply in_list_to_in_list_append_r;apply in_list_cons;
1336                            apply in_list_to_in_list_append_l;assumption
1337                           |apply in_list_to_in_list_append_l;assumption]
1338                        |apply in_remove;assumption]]]]
1339            |split
1340               [intro;apply H7;rewrite > H8;apply in_list_head
1341               |elim (remove_inlist ? ? ? H6);assumption]]
1342         |intro;apply H7;apply in_list_cons;apply in_list_to_in_list_append_l;
1343          assumption
1344         |right;intro;apply H7;apply in_list_cons;
1345          apply in_list_to_in_list_append_r;apply (incl_fv_var ? ? H8)]]]
1346 qed.
1347
1348 lemma fv_NTyp_fv_Typ : ∀T,X,l.(X ∈ (fv_NTyp T)) → ¬(X ∈ l) →
1349                           (X ∈ (fv_type (encodetype T l))).
1350 intros 2;elim T
1351   [simplify;simplify in H;cut (X = n)
1352      [rewrite < Hcut;generalize in match (lookup_in X l);elim (lookup X l)
1353         [elim H1;apply H2;reflexivity
1354         |simplify;apply in_list_head]
1355      |(*FIXME*)generalize in match H;intro;inversion H;intros;
1356         [destruct H4;reflexivity
1357         |destruct H6;elim (not_in_list_nil ? ? H3)]]
1358   |simplify in H;elim (not_in_list_nil ? ? H)
1359   |simplify;simplify in H2;
1360    elim (in_list_append_to_or_in_list ? ? ? ? H2);
1361      [apply in_list_to_in_list_append_l;apply (H ? H4 H3)
1362      |apply in_list_to_in_list_append_r;apply (H1 ? H4 H3)]
1363   |simplify;simplify in H2;
1364    elim (in_list_append_to_or_in_list ? ? ? ? H2)
1365      [apply in_list_to_in_list_append_l;apply (H ? H4 H3)
1366      |apply in_list_to_in_list_append_r;
1367       elim (remove_inlist ? ? ? H4);apply (H1 ? H5);intro;apply H6;
1368       inversion H7;intros
1369         [destruct H9;reflexivity
1370         |destruct H11;elim (H3 H8)]]]
1371 qed.
1372
1373 lemma adeq_WFT : ∀G,T.NWFType G T → WFType (encodeenv G) (encodetype T []).
1374 intros;elim H
1375   [simplify;apply WFT_TFree;rewrite < eq_fv_Nenv_fv_env;assumption
1376   |simplify;apply WFT_Top;
1377   |simplify;apply WFT_Arrow;assumption
1378   |simplify;apply WFT_Forall
1379      [assumption
1380      |intros;rewrite < (encode_subst n2 X n []);
1381         [simplify in H4;apply H4
1382            [rewrite > (eq_fv_Nenv_fv_env l);assumption
1383            |elim (decidable_eq_nat X n)
1384               [left;assumption
1385               |right;intro;apply H6;apply (fv_NTyp_fv_Typ ? ? ? H8);intro;
1386                apply H7;inversion H9;intros
1387                  [destruct H11;reflexivity
1388                  |destruct H13;
1389                   elim (not_in_list_nil ? ? H10)]]]
1390         |4:intro;elim (decidable_eq_nat X n)
1391            [assumption
1392            |elim H6;cut (¬(X ∈ [n]))
1393               [generalize in match Hcut;generalize in match [n];
1394                generalize in match H7;elim n2
1395                  [simplify in H9;generalize in match H9;intro;inversion H9;intros;
1396                     [destruct H13;destruct;simplify;
1397                      generalize in match (lookup_in X l1);elim (lookup X l1)
1398                        [elim H10;apply H12;reflexivity
1399                        |simplify;apply in_list_head]
1400                     |destruct H15;
1401                      elim (not_in_list_nil ? ? H12)]
1402                  |simplify in H9;elim (not_in_list_nil ? ? H9)
1403                  |simplify;simplify in H11;
1404                   elim (in_list_append_to_or_in_list ? ? ? ? H11);autobatch
1405                  |simplify;simplify in H11;
1406                   elim (in_list_append_to_or_in_list ? ? ? ? H11);
1407                     [autobatch
1408                     |elim (remove_inlist ? ? ? H13);
1409                      apply in_list_to_in_list_append_r;
1410                      apply (H10 H14);
1411                      intro;inversion H16;intros;
1412                        [destruct H18;destruct;elim H15;reflexivity
1413                        |destruct H20;elim H12;assumption]]]
1414               |intro;elim H8;inversion H9;intros
1415                  [destruct H11;autobatch
1416                  |destruct H13;elim (not_in_list_nil ? ? H10)]]]
1417         |*:apply not_in_list_nil]]]
1418 qed.
1419
1420 lemma not_in_list_encodetype : \forall T,l,x.in_list ? x l \to
1421                       \lnot (in_list ? x (fv_type (encodetype T l))).
1422 intro;elim T;simplify
1423   [apply (bool_elim ? (lookup n l));intro
1424      [simplify;apply not_in_list_nil
1425      |simplify;intro;inversion H2;intros
1426         [destruct H4;
1427          rewrite > (in_lookup ? ? H) in H1;destruct H1
1428         |destruct H6;apply (not_in_list_nil ? ? H3)]]
1429   |apply not_in_list_nil
1430   |intro;elim (nat_in_list_case ? ? ? H3)
1431      [apply H1;assumption
1432      |apply H;assumption]
1433   |intro;elim (nat_in_list_case ? ? ? H3)
1434      [apply (H1 (n::l) x ? H4);apply in_list_cons;assumption
1435      |apply H;assumption]]
1436 qed.
1437
1438 lemma incl_fv_encode_fv : \forall T,l.incl ? (fv_type (encodetype T l)) (fv_NTyp T).
1439 intro;elim T;simplify;unfold;
1440   [intro;elim (lookup n l)
1441      [simplify in H;elim (not_in_list_nil ? ? H)
1442      |simplify in H;assumption]
1443   |intros;elim (not_in_list_nil ? ? H)
1444   |intros;elim (in_list_append_to_or_in_list ? ? ? ? H2)
1445      [apply in_list_to_in_list_append_l;apply H;autobatch
1446      |apply in_list_to_in_list_append_r;apply H1;autobatch]
1447   |intros;elim (in_list_append_to_or_in_list ? ? ? ? H2)
1448      [apply in_list_to_in_list_append_l;apply H;autobatch
1449      |apply in_list_to_in_list_append_r;apply in_remove
1450         [intro;apply (not_in_list_encodetype n2 (n::l) x)
1451            [rewrite > H4;apply in_list_head
1452            |assumption]
1453         |apply (H1 (n::l));assumption]]]
1454 qed.
1455
1456 lemma adeq_WFT2 : ∀G1,T1.WFType G1 T1 →
1457                      ∀G2,T2.G1 = encodeenv G2 → T1 = encodetype T2 [] →
1458                    NWFType G2 T2.
1459 intros 3;elim H
1460   [rewrite > H2 in H1;rewrite < eq_fv_Nenv_fv_env in H1;
1461    cut (T2 = TName n)
1462      [|generalize in match H3;elim T2
1463         [simplify in H4;destruct H4;reflexivity
1464         |simplify in H4;destruct H4
1465         |simplify in H6;destruct H6
1466         |simplify in H6;destruct H6]]
1467    rewrite > Hcut;apply NWFT_TName;assumption
1468   |cut (T2 = NTop)
1469      [|generalize in match H2;elim T2
1470         [simplify in H3;destruct H3
1471         |reflexivity
1472         |simplify in H5;destruct H5
1473         |simplify in H5;destruct H5]]
1474    rewrite > Hcut;apply NWFT_Top;
1475   |cut (∃U,V.T2 = (NArrow U V))
1476      [|generalize in match H6;elim T2
1477         [1,2:simplify in H7;destruct H7
1478         |apply (ex_intro ? ? n);apply (ex_intro ? ? n1);reflexivity
1479         |simplify in H9;destruct H9]]
1480    elim Hcut;elim H7;rewrite > H8 in H6;simplify in H6;destruct H6;
1481    apply NWFT_Arrow;autobatch
1482   |cut (\exists Z,U,V.T2 = NForall Z U V)
1483      [|generalize in match H6;elim T2
1484         [1,2:simplify in H7;destruct H7
1485         |simplify in H9;destruct H9
1486         |apply (ex_intro ? ? n);apply (ex_intro ? ? n1);
1487          apply (ex_intro ? ? n2);reflexivity]]
1488    elim Hcut;elim H7;elim H8;clear Hcut H7 H8;rewrite > H9;
1489    rewrite > H9 in H6;simplify in H6;destruct H6;apply NWFT_Forall
1490      [autobatch
1491      |intros;elim H6
1492         [rewrite > H7;cut (swap_NTyp a a a2 = a2)
1493            [|elim a2;simplify
1494               [rewrite > swap_same;reflexivity
1495               |reflexivity
1496               |rewrite > H8;rewrite > H9;reflexivity
1497               |rewrite > swap_same;rewrite > H8;rewrite > H9;reflexivity]]
1498          rewrite > Hcut;apply (H4 Y)
1499            [rewrite < eq_fv_Nenv_fv_env;assumption
1500            |rewrite > H7;apply not_in_list_encodetype;
1501             apply in_list_head
1502            |rewrite > H7;simplify;rewrite < Hcut;reflexivity
1503            |rewrite > H7;autobatch]
1504         |apply (H4 Y)
1505            [rewrite < eq_fv_Nenv_fv_env;assumption
1506            |intro;apply H7;apply incl_fv_encode_fv;autobatch
1507            |simplify;reflexivity
1508            |symmetry;apply (encode_subst a2 Y a []);
1509               [3:intro;elim (H7 H8)
1510               |*:autobatch]]]]]
1511 qed.
1512
1513 lemma adeq_WFE : ∀G.NWFEnv G → WFEnv (encodeenv G).
1514 intros;elim H
1515   [simplify;apply WFE_Empty
1516   |simplify;apply WFE_cons;
1517      [2:rewrite < eq_fv_Nenv_fv_env;]
1518    autobatch]
1519 qed.
1520
1521 lemma NWFT_env_incl : ∀G,T.NWFType G T → ∀H.incl ? (fv_Nenv G) (fv_Nenv H)
1522                       → NWFType H T.
1523 intros 3;elim H
1524   [apply NWFT_TName;apply (H3 ? H1)
1525   |apply NWFT_Top
1526   |apply NWFT_Arrow
1527      [apply (H2 ? H6)
1528      |apply (H4 ? H6)]
1529   |apply NWFT_Forall
1530      [apply (H2 ? H6)
1531      |intros;apply (H4 ? ? H8);
1532         [intro;apply H7;apply (H6 ? H9)
1533         |unfold;intros;simplify;simplify in H9;inversion H9;intros
1534            [destruct H11;apply in_list_head
1535            |destruct H13;apply in_list_cons;apply (H6 ? H10)]]]]
1536 qed.
1537
1538 lemma NJSubtype_to_NWFT : ∀G,T,U.NJSubtype G T U → NWFType G T ∧ NWFType G U.
1539 intros;elim H
1540   [split [assumption|apply NWFT_Top]
1541   |split;apply NWFT_TName;assumption
1542   |elim H3;split;
1543      [apply NWFT_TName;generalize in match H1;elim l
1544         [elim (not_in_list_nil ? ? H6)
1545         |inversion H7;intros
1546            [rewrite < H8;simplify;apply in_list_head
1547            |destruct H11;elim t;simplify;apply in_list_cons;
1548             apply H6;assumption]]
1549      |assumption]
1550   |elim H2;elim H4;split;apply NWFT_Arrow;assumption
1551   |elim H2;split;apply NWFT_Forall
1552      [1,3:assumption
1553      |*:intros;elim (H4 Y H7);
1554         [apply (NWFT_env_incl ? ? H9);unfold;simplify;intros;inversion H11;intros
1555            [destruct H13;apply in_list_head
1556            |destruct H15;apply in_list_cons;assumption]
1557         |assumption]]
1558   |elim H2;split
1559      [lapply (adeq_WFT ? ? H5);apply (adeq_WFT2 ? ? Hletin);autobatch
1560      |lapply (adeq_WFT ? ? H6);apply (adeq_WFT2 ? ? Hletin);autobatch]]
1561 qed.
1562
1563 theorem adequacy : ∀G,T,U.NJSubtype G T U →
1564                     JSubtype (encodeenv G) (encodetype T []) (encodetype U []).
1565 intros;elim H;simplify
1566   [1,3,4:autobatch
1567   |apply SA_Refl_TVar
1568      [apply (adeq_WFE ? H1)|rewrite < eq_fv_Nenv_fv_env;assumption]
1569   |apply SA_All
1570      [assumption
1571      |intros;lapply (NSA_All ? ? ? ? ? ? H1 H3);rewrite < (encode_subst n2 X n [])
1572         [rewrite < (encode_subst n4 X n [])
1573            [rewrite < eq_fv_Nenv_fv_env in H5;apply (H4 ? H5)
1574            |2,3:apply not_in_list_nil
1575            |intro;elim (NJSubtype_to_NWFT ? ? ? Hletin);
1576             lapply (in_fvNTyp_in_fvNenv ? ? H8);simplify in Hletin1;
1577             elim (decidable_eq_nat X n)
1578               [assumption
1579               |lapply (in_remove ? ? ? H9 H6);elim H5;rewrite < eq_fv_Nenv_fv_env;
1580                apply Hletin1;apply in_list_to_in_list_append_r;assumption]]
1581         |2,3:apply not_in_list_nil
1582         |intro;elim (NJSubtype_to_NWFT ? ? ? Hletin);lapply (in_fvNTyp_in_fvNenv ? ? H7);
1583          simplify in Hletin1;elim (decidable_eq_nat X n)
1584            [assumption
1585            |lapply (in_remove ? ? ? H9 H6);elim H5;rewrite < eq_fv_Nenv_fv_env;
1586             apply Hletin1;apply in_list_to_in_list_append_r;assumption]]]
1587   |rewrite < (alpha_to_encode ? ? H3);rewrite < (alpha_to_encode ? ? H4);
1588    assumption]
1589 qed.