proposition: Lemma Inj_ex2_can_fun (E := (inductive_limit Injex2_system)): nonempty I -> bijection_prop (Lf (fun z => (P (rep z))) E F) E F.
proof: Proof. move: (Inj_ex2_val) => [eqE eqI eqr eqf] neI. have [eqv esr]:=(inl_equiv_esr Injex2_system). saw; apply: lf_bijective. + move => t /inductive_limitP []; rewrite esr => /inl_sumP [_ ha hb] _. move: hb;rewrite eqE LgV //. + move => u v /inductive_limitP [ha {2} ->] /inductive_limitP [hb {2} ->] sp. rewrite esr in ha hb. by apply: (class_eq1 eqv); apply/Inj_ex2_can_prop. + move: neI => [i iI] y yF. have hu: inc (J y i) (substrate (inl_equiv Injex2_system)). rewrite esr;apply/inl_sumP; aw;rewrite eqE eqI LgV//; split; fprops. exists (class ((inl_equiv Injex2_system)) (J y i)). by apply:inc_class_setQ. by move:(related_rep_class eqv hu); move/Inj_ex2_can_prop => [_ _]; aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)