proposition: Lemma enc_succ n t: enc (S n) t = Succ (enc n t).
proof: Proof. reflexivity. Qed.
imports: RelationClasses Morphisms List Lia Init.Nat Setoid Undecidability.HOU(calculus.calculus second_order.diophantine_equations systemunification nth_order_unification)