proposition: Lemma inl_dl_hlm_fct lm: inc lm r2 -> function_prop (inl_dl_hlm_gen lm) (inl_dl_F_lambda (P lm))(inl_dl_F_lambda (Q lm)).
proof: Proof. move => lemn. move: (pidl_i3_L or2 lemn) => H. have ss: inl_same_index (inl_dl_S_lambda (pidl_i1_L sr2 H)) (inl_dl_S_lambda (pidl_i2_L sr2 H)). by []. move:(proj1 (inl_map2_prop ss (inl_dl_halm_compat H))). move:(pidl_i1_L sr2 H)(pidl_i2_L sr2 H) => p1I p2I. rewrite (inl_dl_F_lambda_prop p1I)(inl_dl_F_lambda_prop p2I). by rewrite /inl_dl_hlm_gen; case: (ixm (inc lm r2)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)