proposition: Lemma enc_app n m t: enc (n + m) t = enc n (enc m t).
proof: Proof. induction n; cbn; simplify; congruence. Qed.
imports: RelationClasses Morphisms List Lia Init.Nat Setoid Undecidability.HOU(calculus.calculus second_order.diophantine_equations systemunification nth_order_unification)