proposition: Lemma Sprod_Il E B x: inc x (Sprod (GE_I E) B) <-> [/\ pairp x, pairp (P x), pairp (Q x), P (P x) = P (Q x) & inc (P (P x)) E /\ inc (J (Q (P x)) (Q (Q x))) B].
proof: Proof. split. move/Sprod_P => [a1 [a2 [b1 [b2 [r1 r2 ->]]]]]. move/GE_I_incP: r1; aw; move => [_ r3 r4];split; fprops. move=> [h1 h2 h3 h4 [h5 h6]]; rewrite -h1 - h2 - h3; apply /Sprod_P. exists (P (P x)), (Q (P x)), (P (Q x)), (Q (Q x)); split => //. apply/GE_I_incP; split; aww. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)