proposition: Lemma list_subset_nil {A} (s : set A) : [::] \subset s.
proof: Proof. intros x Hin. inv Hin. 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)