proposition: Lemma nth_Gamma__deq_F x A: nth Gamma__deq (F x) = Some A -> A = alpha → alpha.
proof: Proof. intros H. eapply nth_error_Some_lt in H as H'. unfold Gamma__deq in *. rewrite tab_nth in H; simplify in *; auto. destruct partition_F_G as [[]| [[[]] ?]]. congruence. exfalso; eapply disjoint_F_G; eauto. Qed.
imports: RelationClasses Morphisms List Lia Init.Nat Setoid Undecidability.HOU(calculus.calculus second_order.diophantine_equations systemunification nth_order_unification)