fact: Fixpoint vars (s: exp X) := match s with | var x => [x] | const x => nil | lambda s => map pred (remove eq_dec 0 (vars s)) | app s1 s2 => vars s1 ++ vars s2 end.
imports: List Lia Undecidability.HOU(calculus.terms calculus.prelim std.std)