proposition: Lemma doubleton_fam_variant x y a b: y <> x -> doubleton_fam (variantL x y a b) a b.
proof: Proof. rewrite /variantL => xny; split; aw; fprops; first by exists x,y; split; fprops. by rewrite Lg_range funI_set2 variant_true // variant_false. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)