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