proposition: Lemma inl_dl_hml_invariant i j (H:gle r2 i j) : inl_dl_hlm H = inl_dl_hlm_gen (J i j).
proof: Proof. rewrite /inl_dl_hlm_gen. case: (ixm (inc (J i j) r2)) => // h. apply:inl_inductive_limit_fun_IV2. - by apply:inl_dl_S_lambda_Iv2; aw. - by apply:inl_dl_S_lambda_Iv2; aw. - by aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)