proposition: Lemma inl_can_fun_fp S i: inc i (isI S) -> function_prop (inl_can_fun S i) (Vg (isE S) i) (inductive_limit S).
proof: Proof. move => ide; rewrite /inl_can_fun. saw; apply:lf_function; exact:inl_can_fun_ax. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)