fact: Definition conseqs e1 e2 := match e1, e2 with | (lambda lambda s1, lambda lambda t1), (lambda lambda s2, lambda lambda t2) => (lambda lambda g s1 s2, lambda lambda g t1 t2) | _, _ => nileq end.
imports: RelationClasses Morphisms Init.Wf List Lia Init.Nat Setoid Undecidability.HOU(calculus.calculus unification.unification)