proposition: Lemma partition_F_G: forall h, { x | F x = h } + { '(x, y, z) | G x y z = h } .
proof: Proof. intros h. unfold F, G. destruct (R__S h) eqn: H1. + left. exists n. rewrite <-H1. now rewrite I__S_R__S. + right. destruct (R__P n) as [a n'] eqn: H2. destruct (R__P n') as [b c] eqn: H3. exists (a, b, c). apply (f_equal I__S) in H1. apply (f_equal I__P) in H2. apply (f_equal I__P) in H3. rewrite ?I__P_R__P, ?I__S_R__S in *. now subst. Qed.
imports: RelationClasses Morphisms List Lia Init.Nat Setoid Undecidability.HOU(calculus.calculus second_order.diophantine_equations systemunification nth_order_unification)