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