fact: Definition SOU n (I: ordsysuni n) := exists (Delta: ctx) (sigma: fin -> exp X), Delta ⊩(n) sigma : Gamma₀' /\ forall s t, (s, t) ∈ E₀' -> sigma • s ≡ sigma • t.
imports: List Lia Morphisms Undecidability.HOU(std.std calculus.calculus unification.higher_order_unification unification.systemunification)