proposition: Lemma two_terms_bij a b f (F:= variantLc a b) : doubleton_fam f a b -> exists g, [/\ bijection g, target g = domain F & f = F \cf (graph g)].
proof: Proof. move => [fgf [x [y [xy df]]] rf]. wlog [qa qb]: x y df xy / Vg f x = a /\ Vg f y = b. move => hyp. move: (set2_1 a b)(set2_2 a b); rewrite - rf. move => /(range_gP fgf) [u udf av] /(range_gP fgf) [v vdf bv]. move: udf vdf; rewrite df => /set2_P a1 /set2_P a2. case: (equal_or_not u v) => cuv. apply: (hyp x y) => //. move: (set2_1 x y)(set2_2 x y); rewrite - df => xdf ydf. move: (inc_V_range fgf xdf) (inc_V_range fgf ydf); rewrite rf. by rewrite av bv cuv => /set1_P -> /set1_P ->. case: a1 => uv; case: a2 => vv. + by case: cuv; rewrite uv vv. + by apply: (hyp x y) => //; rewrite - uv - vv av bv. + by apply: (hyp y x);[rewrite set2_C | apply: nesym | rewrite - uv - vv av bv]. + by case: cuv; rewrite uv vv. move:(set2_equipotent_aux xy); set g := Lf _ _ _; move => [[bg sg tg] ga gb]. rewrite /F;exists g;split;fprops; first by aw. move: (domain_fg (proj1 (proj1 bg))); rewrite sg => dg. apply: fgraph_exten; fprops. by rewrite /composef; aw; rewrite dg. rewrite /composef dg. rewrite df => z; case /set2_P => ->; rewrite LgV //; fprops. by rewrite -/(Vf g x) ga; aw. by rewrite -/(Vf g y) gb; aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)