fact: Definition NU {X: Const} (I: uni X) := exists Delta sigma, Delta ⊩ sigma : Gammaᵤ /\ sigma • sᵤ ≡ sigma • tᵤ /\ forall x, normal (sigma x).
imports: List Lia Undecidability.HOU.calculus(prelim terms syntax semantics equivalence typing order evaluator)