helm/software/matita/contribs/POPLmark/Fsub/adeq.ma

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