proposition: Lemma ex7_can_val_bj : bijection_prop ex7_iso (inductive_limit ex7_system) (inductive_limit S).
proof: Proof. rewrite/ex7_iso ; saw; apply: lf_bijective. - move => x /inductive_limit_hi /= [ha hb _]; apply: inl_class_in_lim => //. move: (ex7_eqv_prop1 ha) => [eqv sr]. by move: hb; rewrite/ex7_Ei_fam/ex7_Ei; rewrite LgV//; move/(rep_i_sr eqv); rewrite sr. - move => x y /inductive_limit_hi /= [iI Px {2} ->]. move => /inductive_limit_hi /= [jI Py {2} ->]. move: (ex7_eqv_prop1 iI) => [eqvi sri]. move: (ex7_eqv_prop1 jI) => [eqvj srj]. move:Px Py; rewrite /ex7_Ei_fam; rewrite!LgV// => Px Py. rewrite - (class_rep eqvi Px) -(class_rep eqvj Py) /ex7_fct. move:(rep_i_sr eqvi Px)(rep_i_sr eqvj Py); rewrite sri srj. set i := Q (rep x); set j := Q (rep y). set x' := rep _; set y' := rep (P (rep y)). move => xE yE /(inl_class_eq_bis iI jI xE yE) [k[]]; aw => lik ljk sv. have x'':inc (class (ex7_eqv i) x') (ex7_Ei i) by apply:inc_class_setQ; ue. have y'':inc (class (ex7_eqv j) y') (ex7_Ei j) by apply:inc_class_setQ; ue. have xE': inc (class (ex7_eqv i) x') (Vg (isE ex7_system) i). rewrite/= /ex7_Ei_fam; rewrite LgV//. have yE': inc (class (ex7_eqv j) y') (Vg (isE ex7_system) j). rewrite/= /ex7_Ei_fam; rewrite LgV//. apply/inl_class_eq_bis => //; exists k; aw; simpl; split => //. rewrite /ex7_fij_fam !LgV//; aw. by rewrite (ex7_fij_ev_bis lik xE) (ex7_fij_ev_bis ljk yE) sv. move => y /inductive_limit_hi [Qx Px ->]; move:Px Qx. set i := Q _; set x := P _; move => xE iI . move:(ex7_eqv_prop1 iI) => [ha hb]. set t := class (ex7_eqv i) x. have tE: inc t (ex7_Ei i) by apply: inc_class_setQ; ue. exists (class (inl_equiv ex7_system) (J t i)). apply:(inl_class_in_lim) => //=; rewrite/ex7_Ei_fam; rewrite LgV//. have tEi: inc t (Vg (isE ex7_system) i) by rewrite /= /ex7_Ei_fam LgV. have [eqv seqv]:= (inl_equiv_esr ex7_system). have jti_s: inc (J t i) (substrate (inl_equiv ex7_system)). rewrite seqv; apply/inl_sumP; aw; split; fprops. move: (related_rep_class eqv jti_s). rewrite /ex7_fct; move/graph_on_P1 => [_ /inl_sumP /= [ {4} <-]]. set i' := Q _; set t' := P _ => iI' tEi';move => [k []] /=; aw => lik lik'. have tE':inc t' (ex7_Ei i') by move: tEi'; rewrite/ex7_Ei_fam; rewrite LgV. move: (ex7_eqv_prop1 iI') => [eqi' sri']. move: (rep_i_sr eqi' tE'); rewrite sri' => rt'E. rewrite /ex7_fij_fam !LgV//;aw. rewrite /t (ex7_fij_ev_bis lik xE)(ex7_fij_ev lik' tE') => eq1. have kI := (proj2(inl_prop0 lik)). move: (ex7_eqv_prop1 kI) => [eqk srk]. move: (inl_prop4 lik) => [fik sik tik]. move: (inl_prop4 lik') => [fik' sik' tik']. have hc: inc (Vf (Vg (isf S) (J i k)) x) (substrate (ex7_eqv k)) by rewrite srk; Wtac. have hd:inc (Vf (Vg (isf S) (J i' k)) (rep t')) (substrate (ex7_eqv k)). by rewrite srk; Wtac. move/(related_equiv_P eqk):(And3 hc hd eq1). move/(ex7_eqv_prop2 kI)=> [_ _]. rewrite inl_class_of_fij // inl_class_of_fij //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)