proposition: Lemma nil_subset {A : Type} (P : set A) : [] \subset P.
proof: Proof. intros x H; inv H. Qed.
imports: mathcomp.ssreflect.ssreflect Classes.RelationClasses Classes.Morphisms List Tactics mathcomp(ssrfun ssrbool ssrnat seq)