proposition: Lemma nil_set_eq {A : Type} : [::] <--> (@set0 A).
proof: Proof. split; move => H; eauto. Qed.
imports: mathcomp.ssreflect.ssreflect Classes.RelationClasses Classes.Morphisms List Tactics mathcomp(ssrfun ssrbool ssrnat seq)