proposition: Lemma setF_pr3 A a: inc A setF -> inc a A -> sub (class (chain_equivalence R E) a) A.
proof: Proof. move:(chain_equivalence_eq A1 A2 A3)=> [es sr]. move=> As aA t /(class_P es) /graph_on_P1 [_ _ ]. apply: (setF_pr2 As aA). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)