proposition: Lemma prl_prop5 S i x: inc i (psI S) -> inc x (Vg (psE S) i) -> Vf (Vg (psf S) (J i i)) x = x.
proof: Proof. by move => iI xE; rewrite (ps_identity_f iI) idV. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)