proposition: Lemma open_abs : forall e u T1, lc (abs T1 e) -> lc u -> lc (open e u).
proof: Proof. intros e u T1 H J. inversion H; subst; auto. rewrite (subst_intro x); auto. apply subst_lc; auto. Qed.
imports: Metalib.Metatheory String