proposition: Lemma inl_dl_hlm_compose l m n (Hlm : gle r2 l m) (Hmn: gle r2 m n): (inl_dl_hlm Hmn) \co (inl_dl_hlm Hlm) = (inl_dl_hlm (proj33 or2 _ _ _ Hlm Hmn)).
proof: Proof. move:(inl_dl_halm_compat Hlm) (inl_dl_halm_compat Hmn). set S1 := (inl_dl_S_lambda (pidl_i1_L sr2 Hlm)). set S2 := (inl_dl_S_lambda (pidl_i2_L sr2 Hlm)). set S3 := (inl_dl_S_lambda (pidl_i1_L sr2 Hmn)). set S4 := (inl_dl_S_lambda (pidl_i2_L sr2 Hmn)). move => h1 h2. have dS2S3: inl_same_data S2 S3 by []. have h1': inl_map2_compat S1 S3 (inl_dl_halm_fam l m) by apply: h1. have sd1: inl_same_index S2 S4 by []. have sd2: inl_same_index S1 S2 by []. rewrite -(proj2(inl_map2_compose sd2 sd1 h1' h2)). rewrite /inl_dl_hlm. set u := Lg _ _. have -> //: u = (inl_dl_halm_fam l n). rewrite /inl_dl_halm_fam /u; apply: Lg_exten => // i iI. by rewrite /inl_dl_halm_fam !LgV//; apply: is_compose_f; apply:inl_dl_index_p2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)