proposition: Lemma setI_subset_compat {U} (s1 s2 s1' s2' : set U) : s1 \subset s1' -> s2 \subset s2' -> (s1 :&: s2) \subset (s1' :&: s2').
proof: Proof. firstorder. Qed.
imports: mathcomp.ssreflect.ssreflect Classes.RelationClasses Classes.Morphisms List Tactics mathcomp(ssrfun ssrbool ssrnat seq)