proposition: Lemma setF_pr4 a: inc a E -> inc (class (chain_equivalence R E) a) setF.
proof: Proof. move=> aE; rewrite /setF. move:(chain_equivalence_eq A1 A2 A3)=> [es sr]. apply: Zo_i. apply/setP_P; rewrite - {2} sr; apply: (sub_class_substrate es). move=> y z ya /setC_P [zE nzc]; dneg yz; apply/(class_P es). move/(class_P es):ya => way; exact: (proj43 es y _ _ way (setF_pr0 yz)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)