proposition: Lemma ex5m_prop1: sub (ex5_mij_J J k x) (substrate (Vg Er k)).
proof: Proof. move => t /funI_P [i iJ ->]. have lij := (proj2 mp2 i iJ). move:(proj1 (ex5_Mij_pr1 lij ((proj33 mp3) i iJ))); rewrite (sEr (proj1 mp2)). by case/(ex5_Xij_pr (Vg x i) lij). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)