proposition: Lemma compat_const c: E (ctype X c) (const c).
proof: Proof. exists (const c); split; [split|]; cbn; intuition. Qed.
imports: Morphisms Lia Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics confluence typing order)