proposition: Lemma inl_map_ax S u F: inl_map_compat S u F -> lf_axiom (inl_map_val u) (inductive_limit S) F.
proof: Proof. move => [p1 p2 p3 p4] x /inductive_limit_hi [ha hb hc]. move:(p3 _ ha) => [fg sg tg]; rewrite /inl_map_val; Wtac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)