proposition: Lemma ex7_fij_prop1' p: inc p (isr S) -> function_prop (Vg ex7_fij_fam p) (Vg ex7_Ei_fam (P p)) (Vg ex7_Ei_fam (Q p)).
proof: Proof. move => pr. move: (pr1_sr pr)(pr2_sr pr); rewrite is_substrate_r => ha hb. move:(proj31 (is_preorder_r S) _ pr) => pp. rewrite / ex7_fij_fam/ex7_Ei_fam ! LgV//. by apply:ex7_fij_prop1; rewrite /gle/related pp. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)