proposition: Lemma ex5_Xij_pr i j x: gle (psr S) i j -> forall t, inc t (ex5_X i j x) <-> (inc t (Vg (psE S) j) /\ x = Vf (ex5_f i j) t).
proof: Proof. by move/(prl_prop4) => [ff sf tf] t; move:(iim_fun_set1_P x ff t); rewrite sf. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)