proposition: Lemma enc_ren delta n s: ren delta (enc n s) = enc n (ren delta s).
proof: Proof. unfold enc; asimpl; now rewrite repeated_map. Qed.
imports: RelationClasses Morphisms List Lia Init.Nat Setoid Undecidability.HOU(calculus.calculus second_order.diophantine_equations systemunification nth_order_unification)