proposition: Lemma eqv_smallest_refl E (R: relation) (R' := fun x y => R x y \/ (inc x E /\ x = y)): (forall x y, R x y -> inc x E /\ inc y E) -> (eqv_smallest E R) = (eqv_smallest E R').
proof: Proof. move => ha. rewrite /eqv_smallest. congr intersection; apply: Zo_exten1 => s /equivalencesP[eq ss]. split => h x y. case; [ by apply: h | by move => [xE <-]; apply:(proj42 eq); rewrite ss ]. by move=> rxy; apply:h; left. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)