proposition: Lemma inl_remark_bijection: bijection_prop (inductive_map inl_remark_S inl_remark_ui inl_remark_U) (inductive_limit inl_remark_S) inl_remark_U.
proof: Proof. have H:=inl_remark_compat. suff: bijection (inductive_map inl_remark_S inl_remark_ui inl_remark_U). by move=>h; split => //; rewrite /inductive_map; aw. split. apply /(inl_map_injective H) => /= i x y iI xFi yFi. have ha:= inl_remark_sub iI. rewrite/inl_remark_ui ! LgV// !ci_V // => ->; exists i => //. by apply: (proj32 or); rewrite sr. apply/(inl_map_surjective H). have hb i: inc i I -> Imf (Vg inl_remark_ui i) = (Vg F i). by move => iI;rewrite /inl_remark_ui LgV//;apply:ci_image;apply:inl_remark_sub. set_extens t. move/setUb_P; rewrite df; move =>[i iI tf]; apply/setUf_P; exists i => //. by rewrite hb. move => /setUf_P [i iI]; rewrite (hb _ iI) => tF. apply/setUb_P; rewrite df; ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)