proposition: Lemma first_proj_classP x y: nonempty y -> forall z, (classp (first_proj_eq x y) z <-> exists2 u, inc u x & z = (singleton u) \times y).
proof: Proof. move=> [y0 y0y]. case:(first_proj_equivalence x y). set (r:=first_proj_eq x y) => er sr. move => z; split. move => cz; move: (proj1 cz); rewrite sr; move /setX_P => [sa sb sc]. exists (P (rep z)) => //. set_extens t => ta. move: (rel_in_class er cz ta) => /first_proj_eq_related_P [qa qb qc]. by move /setX_P: qb => [rq rb rc]; apply /indexedrP. rewrite (proj2 cz); apply /(class_P er); apply /first_proj_eq_related_P. move/indexedrP: ta => [pa pb pc]; split => //; apply /setX_P; split => //; ue. move=> [u uz zp]; rewrite zp. have nep: (nonempty (singleton u \times y)). by exists (J u y0); apply: setXp_i; fprops. move: (rep_i nep); set w:= rep _ => pa. move /indexedrP: (pa) => [ra rb rc]. have wp: inc w (x \times y) by apply /setX_P;split => //; ue. hnf; rewrite - /w; split; first by ue. set_extens t. move /indexedrP => [sa sb sc]; apply /(class_P er). by apply /first_proj_eq_related_P;split; [exact | apply /setX_P |];rewrite sb. move /(class_P er) => /first_proj_eq_related_P [_ /setX_P [qa qb qc] qd]. apply /indexedrP;split => //; ue. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)