fact: Fixpoint size_exp (e1 : exp) {struct e1} : nat := match e1 with | abs e2 => 1 + (size_exp e2) | var_f x1 => 1 | var_b n1 => 1 | app e2 e3 => 1 + (size_exp e2) + (size_exp e3) end.
imports: Coq.Logic.FunctionalExtensionality Coq.Program.Equality Metalib.Metatheory Metalib.LibLNgen Stlc.Definitions