proposition: Lemma ex6_gij_prop1 i j (H:gle rL i j): ex6_gij (J i j) = inl_restr_cf (ex6_prop5c H).
proof: Proof. by rewrite /ex6_gij pr1_pair pr2_pair /inl_restr_cf /inductive_map - ex6_res1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)