proposition: Lemma prl_dl_hlm_fct lm: inc lm r2 -> function_prop (prl_dl_hlm_gen lm) (prl_dl_F_lambda (Q lm))(prl_dl_F_lambda (P lm)).
proof: Proof. move => lemn. move: (pidl_i3_L or2 lemn) => H. move:(proj1 (prl_map2_prop (prl_dl_i12L H) (prl_dl_halm_compat H))). move:(pidl_i1_L sr2 H)(pidl_i2_L sr2 H) => p1I p2I. rewrite (prl_dl_F_lambda_prop p1I)(prl_dl_F_lambda_prop p2I). by rewrite /prl_dl_hlm_gen; case: (ixm (inc lm r2)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)