proposition: Lemma inl_dl2_res1 lam:inc lam I2 -> inl_same_index (inl_dl2_Slambda lam) (inl_dl2_Slambda' lam) /\ inl_map2_compat (inl_dl2_Slambda lam) (inl_dl2_Slambda' lam) (inl_dl2_ulam_fam lam).
proof: Proof. move => li2. rewrite /inl_same_index/inl_map2_compat. set S1 := (inl_dl_S_lambda or1 or2 sr1 sr2 dr1 Sr li2). set S2 := (inl_dl_S_lambda or1 or2 sr1 sr2 dr1 Sr' li2). have [ES1 rS1 fS1]: inl_same_data (inl_dl2_Slambda lam) S1. rewrite/inl_dl2_Slambda/inl_dl_system_S_lambda. by case: (ixm (inc lam I2)). have [ES2 rS2 fS2]: inl_same_data (inl_dl2_Slambda' lam) S2. rewrite/inl_dl2_Slambda'/inl_dl_system_S_lambda. by case: (ixm (inc lam I2)). rewrite/inl_same_index rS1 rS2. split; first exact. have ->: isI (inl_dl2_Slambda lam) = I1. by rewrite - is_domain_E ES1 /= /inl_dl_Elam_fam; aw. rewrite /inl_dl2_ulam_fam ES1 ES2; split. + fprops. + by aw. + move => i iI1; rewrite ! LgV // /= /inl_dl_Elam_fam; aw. have ilI: inc (J i lam) (isI S). by rewrite -is_substrate_r Sr (proj2(pidl_or or1 or2 sr1 sr2)); fprops. exact:(proj43 compat_u _ ilI). + move => i j lij; rewrite fS1 fS2. move:(inl_prop0 lij) => [iI jI]. rewrite /= /inl_dl_glam_fam ! LgV//; aw. apply:(proj44 compat_u (J i lam) (J j lam)). rewrite Sr; apply/pidl_gleP; split;aww. apply:(proj32 or2); ue. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)