proposition: Lemma inl_dl_halm_compat lam mu (H: gle r2 lam mu): inl_map2_compat (inl_dl_S_lambda (pidl_i1_L sr2 H)) (inl_dl_S_lambda (pidl_i2_L sr2 H)) (inl_dl_halm_fam lam mu).
proof: Proof. rewrite /inl_dl_halm_fam;split. - fprops. - by aw. - move => i /= iI; rewrite /inl_dl_Elam_fam ! LgV//. by move:(is_function_f(inl_dl_index_p2 H iI)); aw. - move => i j /= leij. move:(arg1_sr leij)(arg2_sr leij); rewrite sr1 => iI jI. rewrite /inl_dl_glam_fam !LgV //. move:(inl_dl_index_p2 H iI)(inl_dl_index_p2 H jI) => lea led. move: (inl_dl_index_p1 (pidl_i2_L sr2 H) leij); aw => leb. move: (inl_dl_index_p1 (pidl_i1_L sr2 H) leij); aw => lec. by rewrite (is_compose_f lea leb) (is_compose_f lec led). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)