fact: Fixpoint rho (e: exp X) := match e with | var x => var x | const c => const c | lambda s => lambda (rho s) | app (lambda s) t => beta (rho s) (rho t) | app s t => (rho s) (rho t) end.
imports: Morphisms Setoid Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms semantics)