proposition: Lemma inl_restr_cofinal S J (H:cofinal (isr S) J): bijection (inl_restr_cf (cofinal_directed H)).
proof: Proof. set H':= (cofinal_directed H). move:(H) => []; rewrite is_substrate_r => ha hb. have mc:=(inl_restr_cf_compat H'). split. apply/(inl_map_injective mc) => i x y /= iJ; rewrite ! LgV// => xE yE. have iI := (ha _ iJ). rewrite (inl_can_fun_ev iI xE) (inl_can_fun_ev iI yE). move/(inl_class_eq_bis iI iI xE yE) => [k []]; aw => lik _ sv. move: (hb _ (proj2 (inl_prop0 lik))) => [j jI lkj]. move: (f_equal (Vf (Vg (isf S) (Pair.J k j))) sv). rewrite(inl_prop3 lik lkj xE) (inl_prop3 lik lkj yE) => sv'. have lij':gle (induced_order (isr S) J) i j. apply/iorder_gleP; split => //. apply: (proj33 (is_preorder_r S) _ _ _ lik lkj). by exists j => //; rewrite !LgV. move: (inl_restr_cf_compat2 H') => [ff sf tf]. split => //; rewrite sf tf. move => y /inductive_limit_hi [Qi PE ->]. move:(hb _ Qi) => [j jI lij]. rewrite -(inl_class_of_fij lij PE); set x := Vf _ _. have xE: inc x (Vg (isE S) j). move:(inl_prop4 lij) => [fui sui tui]; rewrite/x; Wtac. exists (class (inl_equiv (inl_restr H')) (Pair.J x j)). by apply:inl_class_in_lim => //=; rewrite LgV. by rewrite inl_restr_cf_ev. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)