(*** lemmata on well-formedness ***)
-lemma fv_WFT : \forall T,x,G.(WFType G T) \to (in_list ? x (fv_type T)) \to
- (in_list ? x (fv_env G)).
+lemma fv_WFT : \forall T,x,G.(WFType G T) → x ∈ fv_type T → x ∈ fv_env G.
intros 4.elim H
[simplify in H2;elim (in_list_cons_case ? ? ? ? H2)
[rewrite > H3;assumption|elim (not_in_list_nil ? ? H3)]