proposition: Lemma subconsset T (A : set T) x s : x :: s \subset A <-> x \in A /\ s \subset A.
proof: Proof. split=> [sub|[Ax sub] a [<-|?]] //; last by apply: sub. split=> [|a sa]; apply: sub; first by left. by right. Qed.
imports: mathcomp.ssreflect.ssreflect Classes.RelationClasses Classes.Morphisms List Tactics mathcomp(ssrfun ssrbool ssrnat seq)