proposition: Lemma prl_dl3_ffam_fun ij: inc ij r -> function_prop (Vg prl_dl3_ffam ij) (prl_dl3_Ep (Q ij)) (prl_dl3_Ep (P ij)).
proof: Proof. move => ijr. rewrite /prl_dl3_ffam LgV// /function_prop /ext_map_prod; aw. by split=> //;apply:ext_map_prod_f; apply:prl_dl3_ffam_ax. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)