fact: Definition NSU {X: Const} (I: sysuni X) := exists Delta sigma, Delta ⊩ sigma : Gammaᵤ' /\ (forall s t, (s, t) ∈ Eᵤ' -> sigma • s ≡ sigma • t) /\ forall x, normal (sigma x).
imports: List Lia Undecidability.HOU(std.std calculus.calculus unification.higher_order_unification)