proposition: Lemma inl_product_can_fun_compat S S' (sd: inl_same_index S S'): inl_map_compat (inl_system_product sd) (inl_product_can_fun S S') ((inductive_limit S) \times (inductive_limit S')).
proof: Proof. move:(inl_system_product_prop sd) => [ha hb hc hd]. have ssI := inl_same_index_same_I sd. rewrite /inl_product_can_fun ; split; aww. rewrite ha /inl_product_E; move => i iI; rewrite ! LgV//. by apply:ext_to_prod_fun_bis; apply:inl_can_fun_fp => //; rewrite - ssI. rewrite hc;move => i j lij. move: (inl_prop0 lij) => [iI jI]. rewrite LgV// LgV// hd /inl_product_f LgV//. have jI': inc j (isI S') by rewrite - ssI. have lij': gle (isr S') i j by rewrite - sd. move: (is_function_f lij) (is_function_f lij'); aw => h3 h4. rewrite(ext_to_prod_comp_bis h3 h4 (inl_can_fun_fp jI) (inl_can_fun_fp jI')). by rewrite - (proj2(inl_can_fun_prop lij)) (proj2(inl_can_fun_prop lij')). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)