proposition: Lemma inl_restr_cf_compat S J (H:sub_right_directed J(isr S)): inl_map_compat (inl_restr H) (Lg J (inl_can_fun S)) (inductive_limit S).
proof: Proof. split; aww; simpl. move => i iJ; rewrite !LgV//; apply:inl_can_fun_fp. rewrite - is_substrate_r. exact: (proj1 H _ iJ). move=> i j lij; move /iorder_gleP: (lij)=> [iJ jJ leij]. by rewrite ! LgV // - (proj2 (inl_can_fun_prop leij)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)