proposition: Lemma ex9_map_prop: ex9_map_property ex9_map.
proof: Proof. move:ex9_map_ax => ax. have ra:function_prop ex9_map ex9_quo F. by rewrite /ex9_map; saw; apply: lf_function. split => // i iI. move: ra (function_u iI) => [fa sa ta] [fb sb tb]. move:(ex9_can_fun_fp iI) => [fc sc tc]. move: (chain_equivalence_eq) => [eqv seq]. have cc: ex9_map \coP ex9_can_fun i by split; fprops; ue. apply: function_exten => //; aw; try ue; first by apply:compf_f. rewrite sb => x xEi; rewrite compfV//; last by ue. have xiE: inc (J x i) ex9_G by apply/ex9G_P;split; aww. have ha:inc (Vf (ex9_can_fun i) x) ex9_quo by Wtac. have ax1:= ex9_can_fun_ax iI. rewrite /ex9_map/ex9_map_val LfV //. move: ha;rewrite /ex9_can_fun; rewrite !LfV//. case/ex9_quoP; set y := rep _ => ys eq1. have xiE': inc (J x i) (substrate ex9_rels_ext) by ue. move/(related_equiv_P eqv): (And3 xiE' ys eq1). by move/ex9_map_aux; aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)