proposition: Lemma lc_set_exp_of_lc_exp_size_mutual : forall i1, (forall e1, size_exp e1 = i1 -> lc_exp e1 -> lc_set_exp e1).
proof: Proof. intros i1; pattern i1; apply lt_wf_rec; clear i1; intros i1 H1; apply_mutual_ind exp_mutrec; default_simp; try solve [assert False by default_simp; tauto]; constructor; default_simp; try first [apply lc_set_exp_of_lc_exp]; 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