(* elim vs inversion *)
lemma JS_trans_TFree: ∀G,T,X.G ⊢ T ⊴ (TFree X) →
∀U.G ⊢ (TFree X) ⊴ U → G ⊢ T ⊴ U.
(* elim vs inversion *)
lemma JS_trans_TFree: ∀G,T,X.G ⊢ T ⊴ (TFree X) →
∀U.G ⊢ (TFree X) ⊴ U → G ⊢ T ⊴ U.
lemma fv_append : ∀G,H.fv_env (G @ H) = (fv_env G @ fv_env H).
intro;elim G;simplify;autobatch paramodulation;
lemma fv_append : ∀G,H.fv_env (G @ H) = (fv_env G @ fv_env H).
intro;elim G;simplify;autobatch paramodulation;