proposition: Lemma ord_Gamma__deq: ord' Gamma__deq <= 2.
proof: Proof. unfold Gamma__deq; remember (S (Sum _ + Sum _)) as n. clear Heqn. induction n; cbn; simplify; cbn; auto. rewrite IHn; simplify. destruct (partition_F_G). all: cbn [ord' ord alpha]; auto. Qed.
imports: RelationClasses Morphisms List Lia Init.Nat Setoid Undecidability.HOU(calculus.calculus second_order.diophantine_equations systemunification nth_order_unification)