proposition: Lemma tuto_subset_eqP : forall A B, reflect (A =i B) ((A \subset B) && (B \subset A)).
proof: Proof. move=> A B; apply: (iffP andP) => [[sAB sBA] x| eqAB]. by apply/idP/idP; apply: subsetP. by rewrite !eq_subxx. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finset)