proposition: Lemma char_fun_injectiveP A A' B: sub A B -> sub A' B -> ((A=A') <-> (char_fun A B = char_fun A' B)).
proof: Proof. move=> AB A'B; split => scf; first by rewrite scf. set_extens x => xs; ex_middle u. have xc:= (char_fun_V_b A'B (setC_i (AB _ xs) u)). by case: card1_nz; rewrite -(char_fun_V_a AB xs) scf. have xc:= (char_fun_V_b AB (setC_i (A'B _ xs) u)). by case: card1_nz; rewrite -(char_fun_V_a A'B xs) - scf. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)