proposition: Lemma inl_map2_prop1 S S' u: inl_same_index S S' -> inl_map2_compat S S' u -> inl_map_compat S (inl_map2_aux S' u) (inductive_limit S').
proof: Proof. move => pa pb; move: (pb) => [pd pe pf pg]. have ha:= (inl_same_index_same_I pa). rewrite /inl_map2_aux; split; aww. rewrite - ha;move => i iI; rewrite LgV//. move:(pf _ iI) => [fui sui tui]. rewrite ha in iI. move:(inl_can_fun_fp iI) => [fp sp tp]. by saw; fct_tac; rewrite tui. move => i j le1. case: (inl_prop0 le1) => iI jI. move:(inl_prop4 le1) => [fij sij tij]. move:(pf _ iI) (pf _ jI) => [fui sui tui][fuj suj tuj]. rewrite ha in iI jI. move:(inl_can_fun_fp iI) (inl_can_fun_fp jI) => [fci sci tci][fcj scj tcj]. have co1: inl_can_fun S' i \coP Vg u i by split => //; ue. have co2: inl_can_fun S' j \coP Vg u j by split => //; ue. have ffj: function(inl_can_fun S' j \co Vg u j) by apply: compf_f. have co3:(inl_can_fun S' j \co Vg u j) \coP Vg (isf S) (J i j). split => //; aw; ue. rewrite !LgV//; apply:function_exten. - by apply: compf_f. - by apply: compf_f. - aw; ue. - aw; ue. - aw; rewrite sij => x xE /=. have xe1: inc x (source (Vg u i)) by ue. have xe2: inc x (source (Vg (isf S) (J i j))) by ue. have xe3: inc (Vf (Vg (isf S) (J i j)) x) (source (Vg u j)). by rewrite suj; Wtac. have xe4:inc(Vf (Vg u j) (Vf (Vg (isf S) (J i j)) x)) (Vg (isE S') j) by Wtac. have xe5: inc (Vf (Vg u i) x) (Vg (isE S') i) by Wtac. rewrite ! compfV//. rewrite (inl_can_fun_ev jI xe4) (inl_can_fun_ev iI xe5). symmetry; apply: (inl_map2_compat_prop1 pa pb xE le1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)