proposition: Lemma enc_zero s f: enc 0 s f ≡ s.
proof: Proof. now rewrite enc_app. Qed.
imports: List Lia Undecidability.HOU(std.std calculus.calculus second_order.diophantine_equations) Undecidability.HOU.unification(systemunification nth_order_unification)