proposition: Lemma fin_disj_fam_prop1_bis A x i: fin_disj_fam A -> intp i -> inc x (Vg A i) -> inc x (unionb A) /\ (fin_disj_fam_rank A x) = i.
proof: Proof. move => h iz xx; move: (h) =>[qa qb qc qd]. have xU: inc x (unionb A) by apply/setUb_P; exists i => //; ue. move: (fin_disj_fam_prop1 h xU) =>[pa pb]. split => //; move: (qc (fin_disj_fam_rank A x) i); rewrite qb => h1. case: (h1 pb iz) => // dd; empty_tac1 x. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)