proposition: Lemma Gamma__deq_content A : A ∈ Gamma__deq -> A = alpha → alpha \/ A = alpha → alpha → alpha → alpha.
proof: Proof. intros H; unfold Gamma__deq in *. remember (S (Sum _ + Sum _)) as n. clear Heqn. induction n; cbn in *; intuition. eapply in_app_iff in H; cbn in *; intuition. destruct (partition_F_G); subst; intuition. Qed.
imports: RelationClasses Morphisms List Lia Init.Nat Setoid Undecidability.HOU(calculus.calculus second_order.diophantine_equations systemunification nth_order_unification)