proposition: Lemma inl_map2_compose S S' S'' u v (F := inductive_limit_fun) (w:= Lg (isI S) (fun i => (Vg v i) \co (Vg u i))) : inl_same_index S S' -> inl_same_index S' S'' -> inl_map2_compat S S' u -> inl_map2_compat S' S'' v -> inl_map2_compat S S'' w /\ F S S'' w = F S' S'' v \co F S S' u.
proof: Proof. move => sb1 sb2 hu hv. have sb3: inl_same_index S S'' by rewrite /inl_same_index sb1. move:(inl_map2_prop sb1 hu); rewrite -/F => pa1. move:(inl_map2_prop sb2 hv); rewrite -/F => pa2. move: hu hv=> [cpa1 cpa2 cpa3 cpa4] [cpb1 cpb2 cpb3 cpb4]. have ssI:= inl_same_index_same_I sb1. rewrite - ssI in cpb3. have ha i: inc i (isI S) -> Vg v i \coP Vg u i. move => iI. move: (cpa3 _ iI) (cpb3 _ iI) =>[fu su tu] [fv sv tv]. by split => //;rewrite sv tu. have hb i j: gle (isr S) i j -> Vg u j \coP Vg (isf S) (J i j). move => lij. move:(is_function_f lij)(proj2(inl_prop0 lij)) => [ff sf tf] /cpa3 [fu su tu]. by split => //; rewrite su tf; aw. have hb' i j: gle (isr S') i j -> Vg v j \coP Vg (isf S') (J i j). move => lij; move:(lij); rewrite - sb1 => lij'. move:(is_function_f lij) (cpb3 _ (proj2 (inl_prop0 lij'))). move => [ff sf tf] [fu su tu]. by split => //; rewrite su tf; aw. have hc i j: gle (isr S) i j -> Vg (isf S') (J i j) \coP Vg u i. move => lij; move:(lij); rewrite sb1 => lij'. move:(is_function_f lij') (proj1(inl_prop0 lij))=> [ff sf tf] /cpa3[fu su tu]. by split => //; rewrite sf tu; aw. have hc' i j: gle (isr S) i j -> Vg (isf S'') (J i j) \coP Vg v i. move => lij; move:(lij); rewrite sb1 sb2 => lij'. move: (proj1(inl_prop0 lij))(is_function_f lij')=>/cpb3[fu su tu] [ff sf tf]. by split => //; rewrite sf tu; aw. have cpc:inl_map2_compat S S'' w. rewrite /w; split; aww. move => i iI; rewrite LgV//. move:(cpa3 _ iI) (cpb3 _ iI) => [fu su tu] [fv sv tv]. by saw;fct_tac; rewrite sv tu. move => i j lij. have lij': gle (isr S') i j by rewrite - sb1. move:(inl_prop0 lij)=> [isr jsr]; rewrite ! LgV//. rewrite - (compfA (ha _ jsr) (hb _ _ lij)) - (cpa4 _ _ lij). rewrite (compfA (hb' _ _ lij') (hc _ _ lij)) - (cpb4 _ _ lij'). by rewrite (compfA (hc' _ _ lij) (ha _ isr)). split; first exact. apply:(inl_map2_unique sb3 cpc (inl_map2_prop sb3 cpc)). move: pa1 pa2=> [[ff sf tf] ra2] [ [ff' sf' tf'] ra4]. have ra3: F S' S'' v \coP F S S' u by split => //; rewrite sf' tf. split; first by saw; apply: compf_f. move => i iI. have ssI':= inl_same_index_same_I sb3. have iI': inc i (isI S') by rewrite - ssI. have iI'': inc i (isI S'') by rewrite - ssI'. move: (inl_can_fun_fp iI'') => [fpl'' spl'' tpl'']. move: (inl_can_fun_fp iI') => [fpl' spl' tpl']. move: (inl_can_fun_fp iI) => [fpl spl tpl]. move: (cpb3 _ iI) => [fv sv tv]. move: (cpa3 _ iI) => [fu su tu]. have qa: F S S' u \coP inl_can_fun S i by split => //; ue. have qb: F S' S'' v \coP inl_can_fun S' i by split => //;ue. have qc: inl_can_fun S' i \coP Vg u i by split => //; ue. have qd: inl_can_fun S'' i \coP Vg v i by split => //; ue. rewrite - (compfA ra3 qa) -(ra2 _ iI) (compfA qb qc) - (ra4 _ iI'). rewrite -(compfA qd (ha _ iI)) /w LgV//. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)