proposition: Lemma lin_normal S t: (forall s, s ∈ S -> normal s) -> normal t -> normal (lin S t).
proof: Proof. intros; induction S; cbn; [auto|]. repeat apply normal_app_intro; eauto. Qed.
imports: RelationClasses Morphisms List Lia Init.Nat Setoid Undecidability.HOU(calculus.calculus second_order.diophantine_equations systemunification nth_order_unification)