proposition: Lemma inl_restr_cf_compat2 S J (H:sub_right_directed J(isr S)): function_prop (inl_restr_cf H) (inductive_limit (inl_restr H)) (inductive_limit S).
proof: Proof. exact: (proj1 (inl_map_prop (inl_restr_cf_compat H))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)