proposition: Lemma setIb_identity x: intersectionb (identity_g x) = intersection x.
proof: Proof. rewrite /intersectionb identity_d setI_prop. by apply: setIf_exten; move=> i ix /=; rewrite identity_ev. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)