fact: Definition U (I: uni) := exists (Delta: ctx) (sigma: fin -> exp X), Delta ⊩ sigma : Gammaᵤ /\ sigma • sᵤ ≡ sigma • tᵤ.
imports: List Lia Undecidability.HOU.calculus(prelim terms syntax semantics equivalence typing order evaluator)