proposition: Lemma doubleton_fam_rev a b: doubleton_fam (variantLc b a) a b.
proof: Proof. split; fprops; first by aw; apply: doubleton_C2. by rewrite Lg_range funI_set2 variant_true1 variant_false1 set2_C. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)