proposition: Lemma ex7_fij_prop2 i: inc i (isI S) -> (ex7_fij i i) = identity (ex7_Ei i).
proof: Proof. move => iI. move: (inl_prop1 iI) => lii. apply: (identity_prop0 (ex7_fij_prop1 lii)) => x xEi. move:(ex7_eqv_prop1 iI) => [eqRi sRi]. move: (rep_i_sr eqRi xEi); rewrite sRi => rE. rewrite (ex7_fij_ev lii xEi) (is_identity_f iI) idV//. by apply: class_rep. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)