proposition: Lemma ex6_fct_ax: lf_axiom ex6_fct (inductive_limit ex6_F) (inductive_limit S).
proof: Proof. move => x /ex6_F_prop1 [ha hb hc _]. move: (ex6_prop1 ha hb); rewrite ex6_prop3 => iI. exact:(inl_class_in_lim iI hc). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)