proposition: Lemma subset_respects_set_eq_r : forall (T : Type) (s1 s2 s3 : set T), s3 <--> s2 -> s1 \subset s2 -> s1 \subset s3.
proof: Proof. now firstorder. Qed.
imports: mathcomp.ssreflect.ssreflect Classes.RelationClasses Classes.Morphisms List Tactics mathcomp(ssrfun ssrbool ssrnat seq)