proposition: Lemma inl_map_prop S u F: inl_map_compat S u F -> inl_map_property S u F (inductive_map S u F).
proof: Proof. move => h. move:(inl_map_ax h) => ax. have ra:function_prop (inductive_map S u F) (inductive_limit S) F. by rewrite /inductive_map; saw; apply: lf_function. move: h => [p1 p2 p3 p4]. split => // i iI. move: ra (p3 _ iI) => [fa sa ta] [fb sb tb]. move:(inl_can_fun_fp iI) => [fc sc tc]. have cc: (inductive_map S u F \coP inl_can_fun S i) by split; fprops; ue. apply: function_exten => //; aw; try ue; first by apply:compf_f. rewrite sb => x xEi; rewrite compfV//; last by ue. have xiE: inc (J x i) (inl_sum S) by apply/inl_sumP;split; aww. have ha:inc (Vf (inl_can_fun S i) x) (inductive_limit S) by Wtac. rewrite /inductive_map/inl_map_val LfV//. move: ha; rewrite (inl_can_fun_ev iI xEi). move/inductive_limitP => []; rewrite inl_equiv_sr => yE. move/(inl_class_eq xiE yE) => [k[]]; aw; set y := rep _ => lik ljk sv. rewrite - (f_equal (Vf ^~ x) (p4 _ _ lik)). rewrite - (f_equal (Vf ^~ (P y)) (p4 _ _ ljk)). move:(inl_prop4 lik) => [fik sik tik]. move:(inl_prop4 ljk) => [fjk sjk tjk]. move: (arg2_sr lik); rewrite is_substrate_r => /p3 [fu su tu]. have co1: Vg u k \coP Vg (isf S) (J (Q y) k) by split => //; ue. have co2: Vg u k \coP Vg (isf S) (J i k) by split => //; ue. by rewrite ! compfV//; try ue; rewrite sjk;move /inl_sumP: yE => [_ _]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)