proposition: Lemma setU_set0_neut_eq {A} (s s1 : set A) : s1 <--> set0 -> s <--> s :|: s1.
proof: Proof. firstorder. Qed.
imports: mathcomp.ssreflect.ssreflect Classes.RelationClasses Classes.Morphisms List Tactics mathcomp(ssrfun ssrbool ssrnat seq)