proposition: Lemma inl_rem2_prop2 (u1 := inductive_map S u E') (u2:= inductive_limit_fun S inl_rem2_S' u) (can := Lf (fun z => (P (rep z))) (inductive_limit inl_rem2_S') E'): nonempty (isI S) -> can \coP u2 /\ u1 = can \co u2.
proof: Proof. move => nei. move: (Inj_ex2_can_fun E' (is_preorder_r S) (is_substrate_r S) (@is_directed_r S) nei). rewrite -/can -/inl_rem2_S'; move => [bf sf tf]. move:(inl_map_prop mcu); rewrite -/u1; move =>[[fu1 su1 tu1] u1p]. have ha: inl_same_index S inl_rem2_S' by []. have cc:= inl_rem2_prop1. move:(inl_map2_prop ha cc);rewrite -/u2; move =>[[fu2 su2 tu2] u2p]. have cop: can \coP u2 by split; [ fct_tac | done | ue]. have ax:lf_axiom (fun z => P (rep z)) (inductive_limit inl_rem2_S') E'. by move => t /inductive_limit_hi /= [qa qb _]; move:qb; rewrite LgV//. split => //. apply: function_exten; [ exact | fct_tac | aw; ue | aw; ue | ]. rewrite su1 => x xs. have xu2: inc x (source u2) by ue. have u2x: inc (Vf u2 x) (inductive_limit inl_rem2_S') by Wtac. rewrite /can compfV// LfV //. move/inductive_limit_hi: xs => [pa pb pc]. rewrite pc /u1 inl_inductive_map_ev // inl_map_val_aux2 //. set w := Vf (Vg u (Q (rep x))) (P (rep x)). move: (proj43 mcu _ pa) => [fui sui tui]. have qa: inc (J w (Q (rep x))) (substrate (inl_equiv inl_rem2_S')). rewrite inl_equiv_sr; apply/inl_sumP;split;aww. rewrite LgV ///w; Wtac. move: (related_rep_class (proj1 (inl_equiv_esr inl_rem2_S')) qa). by move/Inj_ex2_can_prop => [_ _]; aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)