proposition: Lemma enc_app n s t: enc n s t ≡ AppL (repeat t n) s.
proof: Proof. unfold enc. do 2 (rewrite stepBeta; asimpl; cbn; trivial). now rewrite !repeated_map; cbn. Qed.
imports: List Lia Undecidability.HOU(std.std calculus.calculus second_order.diophantine_equations) Undecidability.HOU.unification(systemunification nth_order_unification)