proposition: Lemma prl_ne2_im_of_id i: inc i (psI S) -> (Imf (Vg (psf S) (J i i))) = Vg (psE S) i.
proof: Proof. move => iI. move:(identity_f (Vg (psE S) i)) => idp. rewrite (ps_identity_f iI); set_extens t. move/(Imf_P idp); rewrite identity_s; move => [u ua ->]; rewrite idV//. move => tp; apply/(Imf_P idp); rewrite identity_s; ex_tac; rewrite idV //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)