proposition: Lemma lc_exp_of_degree_size_mutual : forall i1, (forall e1, size_exp e1 = i1 -> degree_exp_wrt_exp 0 e1 -> lc_exp e1).
proof: Proof. intros i1; pattern i1; apply lt_wf_rec; clear i1; intros i1 H1; apply_mutual_ind exp_mutind; default_simp; constructor; default_simp; eapply_first_lt_hyp; match goal with | |- _ = _ => reflexivity | _ => idtac end; instantiate; default_simp. Qed.
imports: Coq.Logic.FunctionalExtensionality Coq.Program.Equality Metalib.Metatheory Metalib.LibLNgen Stlc