proposition: Lemma setIrel_sr z e: nonempty z -> (alls z reflexivep) -> (forall r, inc r z -> substrate r = e) -> substrate (intersection z) = e.
proof: Proof. move=> nez allr alls. move: (setIrelR allr)=> ir. set_extens t => ts. move: (ir _ ts); rewrite /related=> aux. move: nez => [u uz]; move: (setI_hi aux uz) => Ju. by rewrite - (alls _ uz); apply: (arg1_sr Ju). have rtt: related (intersection z) t t. apply/(setIrel_P nez) => r rz; rewrite - (alls _ rz) in ts. by apply: (allr _ rz). substr_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)