fact: Definition eq_ordertyping n Gamma e A := Gamma ⊢(n) fst e : A /\ Gamma ⊢(n) snd e : A.
imports: List Lia Morphisms Undecidability.HOU(std.std calculus.calculus unification.higher_order_unification unification.systemunification)