proposition: Lemma enc_add' n m s f: enc (n + m) s f ≡ (enc n) (enc m s f) f.
proof: Proof. induction n; cbn; simplify; [eauto|]. now rewrite IHn. Qed.
imports: List Lia Undecidability.HOU(std.std calculus.calculus second_order.diophantine_equations) Undecidability.HOU.unification(systemunification nth_order_unification)