proposition: Lemma prl_dl3_ffam_id i: inc i I -> Vg prl_dl3_ffam (J i i) = identity (prl_dl3_Ep i).
proof: Proof. move => iI. have rii: inc (J i i) r by apply: (proj32 or); rewrite sr. case: (prl_dl3_ffam_fun rii); aw => ha hb hc. apply:function_exten => //; aww; rewrite hb => x xE. rewrite /prl_dl3_ffam LgV// idV //; aw; rewrite ext_map_prod_V; fprops; last first. by move:(prl_dl3_ffam_ax rii); aw. move: xE; rewrite /prl_dl3_Ep/prl_dl3_Efam => /setXb_P [fgx dx xv]. apply: fgraph_exten; fprops; aw; first by rewrite dx;aw. move => l lL /=;rewrite LgV // /ext_map_prod_aux. have iI': inc i (psI (fS l)) by rewrite -ps_substrate_r (fSr lL) sr. rewrite (ps_identity_f iI') -/(Vf _ _) idV //. by move:(xv l); aw; rewrite LgV//; apply. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)