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