proposition: Lemma enc_mul' n m s f: enc (n * m) s f ≡ (enc n) s (lambda (enc m (var 0) (ren shift f))).
proof: Proof. induction n; cbn. - now simplify. - rewrite enc_add', IHn. simplify. rewrite stepBeta; asimpl; eauto. Qed.
imports: List Lia Undecidability.HOU(std.std calculus.calculus second_order.diophantine_equations) Undecidability.HOU.unification(systemunification nth_order_unification)