proposition: Lemma Gamma__deq_nth_F h: h ∈ Fs E -> nth Gamma__deq h = Some (alpha → alpha).
proof: Proof. intros H. unfold Gamma__deq. rewrite tab_nth. destruct (partition_F_G) as [[x ?]|[[[x y] z] ? ]]; subst; intuition. eapply G_not_in_F in H as []. eapply Sum_in in H. lia. Qed.
imports: RelationClasses Morphisms List Lia Init.Nat Setoid Undecidability.HOU(calculus.calculus second_order.diophantine_equations systemunification nth_order_unification)