proposition: Lemma setF_pr0 a b: R a b -> related (chain_equivalence R E) a b.
proof: Proof. move => rab. move:(A3 rab) (A3 (A2 rab)) => aE bE. by apply/graph_on_P1; split => //;exists (chain_pair a b). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)