proposition: Lemma enc_normal n s: normal s -> normal (enc n s).
proof: Proof. intros; induction n; simplify. - auto. - eapply normal_app_intro; [|eapply normal_app_intro|]; auto. Qed.
imports: RelationClasses Morphisms List Lia Init.Nat Setoid Undecidability.HOU(calculus.calculus second_order.diophantine_equations systemunification nth_order_unification)