proposition: Lemma prl_dl3_or_prop1 p: inc p (prl_dl3_or) -> [/\ pairp p, inc (P p) (I\times L), inc (Q p) (I\times L), inc (J (P (P p)) (P (Q p))) r & (Q (P p)) = (Q (Q p))].
proof: Proof. move => h; move: (proj31(proj1 prl_dl3_osr) _ h) => pp. move: h; rewrite - {1} pp; set x := (P p); set y := Q p. move/prod_of_rel_P => [ha hb hc hd]. move/diagonal_pi_P:(hd) => [_ qq]. move:(arg1_sr hc) (arg2_sr hc) (arg1_sr hd) (arg2_sr hd). by rewrite sr prl_dl3_srL => qa qb qc qd;split => //;apply/ setX_P. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)