+ |elim H5;autobatch depth=4]]]]
+qed.
+
+let rec closed_type T n ≝
+ match T with
+ [ TVar m ⇒ m < n
+ | TFree X ⇒ True
+ | Top ⇒ True
+ | Arrow T1 T2 ⇒ closed_type T1 n ∧ closed_type T2 n
+ | Forall T1 T2 ⇒ closed_type T1 n ∧ closed_type T2 (S n)].
+
+lemma decoder : ∀T,n.closed_type T n →
+ ∀l.length ? l = n → distinct_list l →
+ (\forall x. x ∈ (fv_type T) \to x ∉ l) \to
+ ∃U.T = encodetype U l.
+intro;elim T
+ [simplify in H;apply (ex_intro ? ? (TName (nth ? l O n)));simplify;
+ rewrite > lookup_nth;simplify;autobatch;
+ |apply (ex_intro ? ? (TName n));rewrite > (fv_encode (TName n) l []);
+ [simplify;reflexivity
+ |intros;simplify in H3;simplify in H4;lapply (H3 ? H4);
+ cut (lookup x l = false)
+ [rewrite > Hcut;simplify;split
+ [reflexivity|intro;destruct H5]
+ |elim (bool_to_decidable_eq (lookup x l) true)
+ [lapply (lookup_in ? ? H5);elim (Hletin Hletin1)
+ |generalize in match H5;elim (lookup x l);
+ [elim H6;reflexivity|reflexivity]]]]
+ |apply (ex_intro ? ? NTop);simplify;reflexivity
+ |simplify in H2;elim H2;lapply (H ? H6 ? H3 H4);
+ [lapply (H1 ? H7 ? H3 H4)
+ [elim Hletin;elim Hletin1;
+ apply (ex_intro ? ? (NArrow a a1));autobatch;
+ |intros;apply H5;simplify;autobatch]
+ |intros;apply H5;simplify;autobatch]
+ |simplify in H2;elim H2;elim (H ? H6 ? H3 H4);elim (fresh_name (fv_type t1@l));
+ [elim (H1 ? H7 (a1::l))
+ [apply (ex_intro ? ? (NForall a1 a a2));simplify;autobatch
+ |simplify;autobatch
+ |unfold;intros;intro;apply H12;generalize in match H13;generalize in match H10;
+ generalize in match H11;generalize in match H9;
+ generalize in match m;generalize in match n1;
+ apply nat_elim2
+ [intro;elim n2
+ [reflexivity
+ |simplify in H18;rewrite > H18 in H9;elim H9;simplify in H16;
+ lapply (le_S_S_to_le ? ? H16);autobatch depth=4]
+ |intro;intros;change in H17:(? ? % ?) with (nth nat l O n2);
+ simplify in H17:(? ? ? %);elim H9;rewrite < H17;
+ apply in_list_to_in_list_append_r;apply nth_in_list;
+ simplify in H16;autobatch
+ |intros;change in H18 with (nth nat l O n2 = nth nat l O m1);
+ unfold in H4;elim (decidable_eq_nat n2 m1)
+ [autobatch
+ |simplify in H17;simplify in H16;elim (H4 ? ? ? ? H19);autobatch]]
+ |intro;elim (in_list_cons_case ? ? ? ? H11)
+ [apply H9;apply in_list_to_in_list_append_l;rewrite < H12;assumption
+ |apply (H5 x);simplify;autobatch]]
+ |apply H5;simplify;autobatch]]
+qed.
+
+lemma closed_subst : \forall T,X,n.closed_type (subst_type_nat T (TFree X) n) n
+ \to closed_type T (S n).
+intros 2;elim T 0;simplify;intros
+ [elim (decidable_eq_nat n n1)
+ [rewrite > H1;apply le_n
+ |rewrite > (not_eq_to_eqb_false ? ? H1) in H;simplify in H;
+ apply le_S;assumption]
+ |2,3:apply I
+ |elim H2;split;autobatch
+ |elim H2;split;autobatch]
+qed.
+
+lemma WFT_to_closed: ∀G,T.WFType G T → closed_type T O.
+intros;elim H;simplify
+ [1,2:apply I
+ |split;assumption
+ |split
+ [assumption
+ |elim (fresh_name (fv_env l@fv_type t1));lapply (H4 a)
+ [autobatch
+ |*:intro;autobatch]]]
+qed.
+
+lemma adeq_WFE2 : ∀G1.WFEnv G1 → ∀G2.(G1 = encodeenv G2) → NWFEnv G2.
+intros 2;elim H 0
+ [intro;elim G2
+ [apply NWFE_Empty
+ |simplify in H2;destruct H2]
+ |intros 9;elim G2
+ [simplify in H5;destruct H5
+ |elim a in H6;simplify in H6;destruct H6;apply NWFE_cons;autobatch]]
+qed.
+
+lemma in_list_encodeenv : \forall b,X,T,l.
+ in_list ? (mk_bound b X (encodetype T [])) (encodeenv l) \to
+ \exists U.encodetype U [] = encodetype T [] \land
+ (mk_nbound b X U) ∈ l.
+intros 4;elim l
+ [simplify in H;elim (not_in_list_nil ? ? H)
+ |simplify in H1;inversion H1;elim a 0;simplify;intros;destruct;
+ [apply (ex_intro ? ? n1);split;autobatch
+ |elim (H H2);elim H4;apply (ex_intro ? ? a1);split;autobatch]]
+qed.
+
+lemma eq_swap_NTyp_to_case :
+ \forall X,Y,Z,T. Y ∉ (X::var_NTyp T) \to
+ swap_NTyp Z Y (swap_NTyp Y X T) = swap_NTyp Z X T \to
+ Z = X \lor Z ∉ (fv_NTyp T).
+intros 4;elim T
+ [simplify in H;simplify in H1;elim (decidable_eq_nat X n)
+ [rewrite > H2;simplify;elim (decidable_eq_nat Z n)
+ [left;assumption
+ |right;intro;apply H3;apply in_list_singleton_to_eq;assumption]
+ |elim (decidable_eq_nat Y n)
+ [elim H;autobatch;
+ |rewrite > (swap_other Y X n) in H1
+ [elim (decidable_eq_nat Z n)
+ [rewrite > H4 in H1;do 2 rewrite > swap_left in H1;
+ destruct H1;elim H;apply in_list_head
+ |elim (decidable_eq_nat Z X)
+ [left;assumption
+ |rewrite > (swap_other Z X n) in H1
+ [right;intro;apply H3;simplify in H6;
+ rewrite > (in_list_singleton_to_eq ? ? ? H6) in H1;
+ rewrite > swap_left in H1;destruct H1;reflexivity
+ |*:intro;autobatch]]]
+ |*:intro;autobatch]]]
+ |simplify;right;apply not_in_list_nil
+ |elim H
+ [left;assumption
+ |elim H1
+ [left;assumption
+ |right;simplify;intro;elim (in_list_append_to_or_in_list ? ? ? ? H6)
+ [elim (H4 H7)
+ |elim (H5 H7)]
+ |intro;apply H2;simplify;inversion H5;intros;destruct;autobatch;
+ |simplify in H3;destruct H3;assumption]
+ |intro;apply H2;simplify;inversion H4;intros;destruct;autobatch
+ |simplify in H3;destruct H3;assumption]
+ |elim H
+ [left;assumption
+ |elim H1
+ [left;assumption
+ |right;simplify;intro;elim (in_list_append_to_or_in_list ? ? ? ? H6)
+ [elim (H4 H7)
+ |elim H5;elim (remove_inlist ? ? ? H7);assumption]
+ |intro;apply H2;simplify;inversion H5;intros;destruct;autobatch
+ |simplify in H3;destruct H3;assumption]
+ |intro;apply H2;simplify;inversion H4;intros;destruct;autobatch depth=4;
+ |simplify in H3;destruct H3;assumption]]
+qed.
+
+
+theorem faithfulness : ∀G1,T1,U1.G1 ⊢ T1 ⊴ U1 →
+ ∀G2,T2,U2.
+ G1 = encodeenv G2 →
+ T1 = encodetype T2 [] →
+ U1 = encodetype U2 [] →
+ NJSubtype G2 T2 U2.
+intros 4;elim H 0
+ [intros;cut (U2 = NTop)
+ [|generalize in match H5;elim U2 0;simplify;intros;destruct;reflexivity]
+ rewrite > Hcut;apply NSA_Top;autobatch;
+ |intros;cut (T2 = TName n ∧ U2 = TName n)
+ [|split
+ [elim T2 in H4 0;simplify;intros;destruct;reflexivity
+ |elim U2 in H5 0;simplify;intros;destruct;reflexivity]]
+ elim Hcut;
+ rewrite > H6;rewrite > H7;apply NSA_Refl_TVar;
+ [autobatch
+ |rewrite > H3 in H2;rewrite < eq_fv_Nenv_fv_env in H2;assumption]
+ |intros;cut (T2 = TName n)
+ [|elim T2 in H5 0;simplify;intros;destruct;reflexivity]
+ rewrite > Hcut;elim (decoder t1 O ? []);
+ [rewrite > H4 in H1;rewrite > H7 in H1;elim (in_list_encodeenv ???? H1);
+ elim H8;autobatch
+ |4:unfold;intros;simplify in H7;elim (not_le_Sn_O ? H7)
+ |*:autobatch]
+ |intros;cut (∃u,u1,u2,u3.T2 = NArrow u u1 ∧ U2 = NArrow u2 u3)
+ [decompose;rewrite > H8;rewrite > H10;rewrite > H10 in H7;simplify in H7;destruct;
+ simplify in H6;destruct;autobatch width=4 size=9
+ |generalize in match H6;elim T2 0;simplify;intros;destruct;
+ generalize in match H7;elim U2 0;simplify;intros;destruct;
+ autobatch depth=6 width=2 size=7]
+ |intros;cut (∃n,u,u1,n1,u2,u3.T2 = NForall n u u1 ∧ U2 = NForall n1 u2 u3)
+ [decompose;rewrite > H8;rewrite > H10;
+ rewrite > H8 in H6;rewrite > H10 in H7;simplify in H6;simplify in H7;
+ destruct;lapply (SA_All ? ? ? ? ? H1 H3);
+ lapply (JS_to_WFT1 ? ? ? Hletin);lapply (JS_to_WFT2 ? ? ? Hletin);
+ apply NSA_All
+ [autobatch;
+ |intros;apply H4;
+ [apply Z
+ |2,3:autobatch
+ |rewrite < (encode_subst a2 Z a []);
+ [1,2,3:autobatch
+ |lapply (SA_All ? ? ? ? ? H1 H3);lapply (JS_to_WFT1 ? ? ? Hletin);
+ intro;elim (decidable_eq_nat Z a)
+ [assumption
+ |lapply (fv_WFT ? Z ? Hletin1)
+ [elim H5;autobatch
+ |simplify;apply in_list_to_in_list_append_r;
+ apply fv_NTyp_fv_Typ
+ [assumption
+ |intro;autobatch]]]]
+ |rewrite < (encode_subst a5 Z a3 [])
+ [1,2,3:autobatch
+ |intro;elim H7;autobatch]]]
+ |generalize in match H6;elim T2 0;simplify;intros;destruct;
+ generalize in match H7;elim U2 0;simplify;intros;destruct;
+ autobatch depth=8 width=2 size=9]]
+qed.
+
+theorem NJS_trans : ∀G,T,U,V.NJSubtype G T U → NJSubtype G U V → NJSubtype G T V.
+intros;apply faithfulness [5,6,7:autobatch|4:autobatch|*:skip]