proposition: Lemma Inj_ex2_can_prop x y (E := (inl_sum Injex2_system)): related (inl_equiv Injex2_system) x y <-> [/\ inc x E, inc y E & P x = P y].
proof: Proof. move: (Inj_ex2_val) => [eqE eqI eqr eqf]. split. move/graph_on_P1 =>[xE yE [k [ka kb kc]]]; split => //. move/inl_sumP:xE;move/inl_sumP:yE;rewrite eqI eqE. move => [_ qy py][_ qx px]; move: py px; rewrite !LgV// => py px. move: kc; rewrite eqf ! LgV //! idV//. move => [xE yE sp]; apply/graph_on_P1; split => //. move/inl_sumP:xE;move/inl_sumP:yE;rewrite eqI eqE. move => [_ qy py][_ qx px]; move: py px; rewrite !LgV// => py px. move:(rdr qx qy) => [k [kI ka kb]]. exists k; rewrite eqr eqf ! LgV // !idV //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)