proposition: Lemma list_subset_cons {A} (h : A) (t : seq A) (s : set A) : s h -> t \subset s -> (h :: t) \subset s.
proof: Proof. intros H1 H2 x Hin. inv Hin; eauto. Qed.
imports: String micromega.Lia List Tactics TacticsUtil Instances Classes DependentClasses Sets Producer Enumerators Checker Decidability CheckerProofs Ltac2(Ltac2) mathcomp(ssreflect ssrfun ssrbool ssrnat eqtype seq)