proposition: Lemma inl_dl_F_lambda_prop lam (Hl: inc lam I2): inl_dl_F_lambda lam = inductive_limit (inl_dl_S_lambda Hl).
proof: Proof. rewrite /inl_dl_F_lambda /inl_dl_system_S_lambda. by case: (ixm (inc lam I2)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)