proposition: Lemma cons_subset {A : Type} (x : A) (l : seq A) (P : set A) : P x -> l \subset P -> (x :: l) \subset P.
proof: Proof. intros Px Pl x' Hin. inv Hin; firstorder. Qed.
imports: mathcomp.ssreflect.ssreflect Classes.RelationClasses Classes.Morphisms List Tactics mathcomp(ssrfun ssrbool ssrnat seq)