proposition: Lemma subset_eqP T (A B : set T) : (A <--> B) <-> (A \subset B /\ B \subset A).
proof: Proof. split; first by move=> eqAB; split=> a; rewrite (eqAB a). by case=> subAB subBA a; split; [apply: subAB | apply:subBA]. Qed.
imports: mathcomp.ssreflect.ssreflect Classes.RelationClasses Classes.Morphisms List Tactics mathcomp(ssrfun ssrbool ssrnat seq)