+lemma NJS_fv_to_fvNenv : ∀G,T,U.NJSubtype G T U →
+ fv_NTyp T ⊆ fv_Nenv G ∧ fv_NTyp U ⊆ fv_Nenv G.
+intros;elim H;simplify;
+[split
+ [autobatch
+ |unfold;intros;elim (not_in_list_nil ?? H3)]
+|split;unfold;intros;rewrite > (in_list_singleton_to_eq ??? H3);assumption
+|decompose;split;try autobatch;unfold;intros;
+ rewrite > (in_list_singleton_to_eq ??? H3);
+ generalize in match (refl_eq ? (mk_nbound true n n2));
+ elim H1 in ⊢ (???% → %)
+ [rewrite < H6;simplify;apply in_list_head
+ |cases a1;cases b;simplify;
+ [apply in_list_cons;apply H7;assumption
+ |apply H7;assumption]]
+|decompose;split;unfold;intros;
+ [elim (in_list_append_to_or_in_list ???? H4);autobatch
+ |elim (in_list_append_to_or_in_list ???? H4);autobatch]
+|decompose;split;unfold;intros;
+ [elim (in_list_append_to_or_in_list ? ? ? ? H2)
+ [autobatch
+ |elim (fresh_name (x::fv_Nenv l@var_NTyp n3@var_NTyp n5));lapply (H4 a)
+ [cut (a ≠ x ∧ x ≠ n)
+ [elim Hcut;elim Hletin;lapply (H11 x)
+ [simplify in Hletin1;inversion Hletin1;intros;destruct;
+ [elim Hcut;elim H13;reflexivity
+ |assumption]
+ |elim n3 in H7 H8
+ [simplify in H7;elim (decidable_eq_nat n n6)
+ [rewrite > (eq_to_eqb_true ? ? H13) in H7;simplify in H7;
+ elim (not_in_list_nil ? ? H7)
+ |rewrite > (not_eq_to_eqb_false ? ? H13) in H7;
+ simplify in H7;inversion H7;intros
+ [destruct;simplify;rewrite > swap_other
+ [apply in_list_head
+ |intro;apply H8;rewrite > H14;autobatch
+ |intro;apply H13;rewrite > H14;reflexivity]
+ |destruct;elim (not_in_list_nil ? ? H14)]]
+ |simplify in H7;elim (not_in_list_nil ? ? H7)
+ |simplify in H14;simplify;elim (remove_inlist ? ? ? H13);
+ simplify in H15;elim (in_list_append_to_or_in_list ? ? ? ? H15)
+ [apply in_list_to_in_list_append_l;apply H7
+ [apply (in_remove ? ? ? H16 H17)
+ |intro;apply H14;simplify;
+ rewrite < (associative_append ? [x] (fv_Nenv l) ((var_NTyp n6 @ var_NTyp n7)@var_NTyp n5));
+ elim (in_list_append_to_or_in_list ? ? (x::fv_Nenv l) (var_NTyp n6@var_NTyp n5) H18);
+ [apply in_list_to_in_list_append_l;apply H19
+ |apply in_list_to_in_list_append_r;
+ elim (in_list_append_to_or_in_list ???? H19);autobatch]]
+ |apply in_list_to_in_list_append_r;apply H8
+ [apply (in_remove ? ? ? H16 H17)
+ |intro;apply H14;simplify;
+ rewrite < (associative_append ? [x] (fv_Nenv l) ((var_NTyp n6 @ var_NTyp n7)@var_NTyp n5));
+ elim (in_list_append_to_or_in_list ? ? (x::fv_Nenv l) (var_NTyp n7@var_NTyp n5) H18);
+ [apply in_list_to_in_list_append_l;apply H19
+ |apply in_list_to_in_list_append_r;
+ elim (in_list_append_to_or_in_list ???? H19);autobatch]]]
+ |simplify in H14;simplify;elim (remove_inlist ? ? ? H13);
+ simplify in H15;elim (in_list_append_to_or_in_list ? ? ? ? H15)
+ [apply in_list_to_in_list_append_l;apply H7
+ [apply (in_remove ? ? ? H16 H17)
+ |intro;apply H14;simplify;
+ rewrite < (associative_append ? [x] (fv_Nenv l) (n6::(var_NTyp n7 @ var_NTyp n8)@var_NTyp n5));
+ elim (in_list_append_to_or_in_list ? ? (x::fv_Nenv l) (var_NTyp n7@var_NTyp n5) H18);
+ [apply in_list_to_in_list_append_l;apply H19
+ |apply in_list_to_in_list_append_r;apply in_list_cons;
+ elim (in_list_append_to_or_in_list ???? H19);autobatch]]
+ |apply in_list_to_in_list_append_r;apply in_remove;
+ [elim (remove_inlist ??? H13);intro;apply H19;
+ elim (swap_case a n n6)
+ [elim H21
+ [elim H14;rewrite < H22;rewrite < H20;apply in_list_head
+ |autobatch paramodulation]
+ |elim (remove_inlist ??? H17);elim H23;autobatch paramodulation]
+ |apply H8
+ [apply (in_remove ? ? ? H16);elim (remove_inlist ??? H17);assumption
+ |intro;apply H14;simplify;
+ rewrite < (associative_append ? [x] (fv_Nenv l) (n6::(var_NTyp n7 @ var_NTyp n8)@var_NTyp n5));
+ elim (in_list_append_to_or_in_list ? ? (x::fv_Nenv l) (var_NTyp n8@var_NTyp n5) H18);
+ [apply in_list_to_in_list_append_l;apply H19
+ |apply in_list_to_in_list_append_r;apply in_list_cons;
+ elim (in_list_append_to_or_in_list ???? H19);autobatch]]]]]]
+ |split
+ [intro;apply H8;rewrite > H9;apply in_list_head
+ |elim (remove_inlist ? ? ? H7);assumption]]
+ |intro;autobatch depth=4
+ |3,4:intro;elim H8;apply in_list_cons;autobatch depth=4]]
+ |elim (in_list_append_to_or_in_list ? ? ? ? H2)
+ [autobatch
+ |elim (fresh_name (x::fv_Nenv l@var_NTyp n3@var_NTyp n5));lapply (H4 a)
+ [cut (a ≠ x ∧ x ≠ n1)
+ [elim Hcut;elim Hletin;lapply (H12 x)
+ [simplify in Hletin1;inversion Hletin1;intros;destruct;
+ [elim Hcut;elim H13;reflexivity
+ |assumption]
+ |elim n5 in H7 H8
+ [simplify in H7;elim (decidable_eq_nat n1 n6)
+ [rewrite > (eq_to_eqb_true ? ? H13) in H7;simplify in H7;
+ elim (not_in_list_nil ? ? H7)
+ |rewrite > (not_eq_to_eqb_false ? ? H13) in H7;
+ simplify in H7;inversion H7;intros
+ [destruct;simplify;rewrite > swap_other
+ [apply in_list_head
+ |intro;apply H8;rewrite > H14;autobatch
+ |intro;apply H13;rewrite > H14;reflexivity]
+ |destruct;elim (not_in_list_nil ? ? H14)]]
+ |simplify in H7;elim (not_in_list_nil ? ? H7)
+ |simplify in H14;simplify;elim (remove_inlist ? ? ? H13);
+ simplify in H15;elim (in_list_append_to_or_in_list ? ? ? ? H15)
+ [apply in_list_to_in_list_append_l;apply H7
+ [apply (in_remove ? ? ? H16 H17)
+ |intro;apply H14;simplify;
+ rewrite < (associative_append ? [x] (fv_Nenv l) (var_NTyp n3 @ var_NTyp n6@var_NTyp n7));
+ elim (in_list_append_to_or_in_list ? ? (x::fv_Nenv l) (var_NTyp n3@var_NTyp n6) H18);
+ [apply in_list_to_in_list_append_l;apply H19
+ |apply in_list_to_in_list_append_r;
+ elim (in_list_append_to_or_in_list ???? H19);autobatch]]
+ |apply in_list_to_in_list_append_r;apply H8
+ [apply (in_remove ? ? ? H16 H17)
+ |intro;apply H14;simplify;
+ rewrite < (associative_append ? [x] (fv_Nenv l) (var_NTyp n3 @ var_NTyp n6@var_NTyp n7));
+ elim (in_list_append_to_or_in_list ? ? (x::fv_Nenv l) (var_NTyp n3@var_NTyp n7) H18);
+ [apply in_list_to_in_list_append_l;apply H19
+ |apply in_list_to_in_list_append_r;
+ elim (in_list_append_to_or_in_list ???? H19);autobatch]]]
+ |simplify in H14;simplify;elim (remove_inlist ? ? ? H13);
+ simplify in H15;elim (in_list_append_to_or_in_list ? ? ? ? H15)
+ [apply in_list_to_in_list_append_l;apply H7
+ [apply (in_remove ? ? ? H16 H17)
+ |intro;apply H14;simplify;
+ rewrite < (associative_append ? [x] (fv_Nenv l) (var_NTyp n3@n6::var_NTyp n7 @ var_NTyp n8));
+ elim (in_list_append_to_or_in_list ? ? (x::fv_Nenv l) (var_NTyp n3@var_NTyp n7) H18);
+ [apply in_list_to_in_list_append_l;apply H19
+ |apply in_list_to_in_list_append_r;
+ elim (in_list_append_to_or_in_list ???? H19);autobatch depth=4]]
+ |apply in_list_to_in_list_append_r;apply in_remove;
+ [elim (remove_inlist ??? H13);intro;apply H19;
+ elim (swap_case a n1 n6)
+ [elim H21
+ [elim H14;rewrite < H22;rewrite < H20;apply in_list_head
+ |autobatch paramodulation]
+ |elim (remove_inlist ??? H17);elim H23;autobatch paramodulation]
+ |apply H8
+ [apply (in_remove ? ? ? H16);elim (remove_inlist ??? H17);assumption
+ |intro;apply H14;simplify;
+ rewrite < (associative_append ? [x] (fv_Nenv l) (var_NTyp n3@n6::var_NTyp n7 @ var_NTyp n8));
+ elim (in_list_append_to_or_in_list ? ? (x::fv_Nenv l) (var_NTyp n3@var_NTyp n8) H18);
+ [apply in_list_to_in_list_append_l;apply H19
+ |apply in_list_to_in_list_append_r;
+ elim (in_list_append_to_or_in_list ???? H19);autobatch depth=4]]]]]]
+ |split
+ [intro;apply H8;rewrite > H9;apply in_list_head
+ |elim (remove_inlist ? ? ? H7);assumption]]
+ |intro;autobatch depth=4
+ |3,4:intro;elim H8;apply in_list_cons;autobatch depth=4]]]]