proposition: Lemma prl_dl3_ffam_ax ij: inc ij r -> ext_map_prod_axioms L (fun l : Set => Vg (psE (fS l)) (Q ij)) (fun l => Vg (psE (fS l)) (P ij)) (fun l => graph (Vg (psf (fS l)) ij)).
proof: Proof. move => ijr l lL. rewrite - (fSr lL) in ijr. move:(ps_function_f ijr); set f:= Vg _ _; set Ej := Vg _ _; set Ei := Vg _ _. by move => [[/corr_propc /proj33 ha hb hc] <- <-]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)