proposition: Lemma singl_set_eq: forall (A : Type) (x : A), [ x ] <--> [ set x ].
proof: Proof. intros A x x'; split; intros H. - inv H. reflexivity. now inv H0. - inv H. now constructor. Qed.
imports: mathcomp.ssreflect.ssreflect Classes.RelationClasses Classes.Morphisms List Tactics mathcomp(ssrfun ssrbool ssrnat seq)