proposition: Lemma GE_J_range E : range (GE_J E) = (E\times (E\times E)).
proof: Proof. apply: extensionality => x. move /funI_P => [z /GE_J_P [a [b [c [ha hb hc eq]]]] ->]. by rewrite eq pr2_pair; apply: setXp_i => //; apply: setXp_i. move=> /setX_P [pa pe /setX_P[pb pc pd]]; apply/funI_P. exists (J (J (J (P x) (P (Q x))) (Q (Q x))) x); aw; trivial. by rewrite - {4} pa - {3} pb;apply/GE_J_P; exists (P x),(P (Q x)), (Q (Q x)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)