fact: Definition encodes s n := forall t delta, (ren delta s) t ≡ enc n t.
imports: RelationClasses Morphisms List Lia Init.Nat Setoid Undecidability.HOU(calculus.calculus second_order.diophantine_equations systemunification nth_order_unification)