proposition: Lemma setIf_S f: {compat (intersectionf ^~ f) : x y / sub x y /\ nonempty x >-> sub y x}.
proof: Proof. move=> A B [sAB neA]. have neB: (nonempty B) by move:neA=> [x]; exists x; apply: sAB. by move=> x /(setIf_P _ neB) p; apply:(setIf_i neA) =>j jA; apply:p; apply: sAB. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)