proposition: Lemma subst_lc_c_alternate_proof : forall (x : atom) u e, lc_c e -> lc_c u -> lc_c ([x ~> u] e).
proof: Proof. intros x u e He Hu. induction He. Case "fvar". simpl. destruct (x0 == x). auto. auto. Case "abs". simpl. pick fresh y and apply lc_abs_c. rewrite subst_open_var_c. auto. auto. auto. Case "app". simpl. auto. Qed.
imports: Metalib.Metatheory String