proposition: Lemma inl_dl_hml_id i: inc i I2 -> Vg (Lg r2 inl_dl_hlm_gen) (J i i) = identity (inl_dl_F_lambda i).
proof: Proof. move => i2. have iir: inc (J i i) r2 by apply: (proj32 or2 i); rewrite sr2. rewrite LgV // inl_dl_F_lambda_prop. set S1 := (inl_dl_S_lambda (pidl_i1_L sr2 iir)). set S2 := (inl_dl_S_lambda (pidl_i2_L sr2 iir)). have ha: (inl_same_index S1 S2) by []. have hb:=(inl_dl_halm_compat iir). move:(inl_map2_prop ha hb). set f := inductive_limit_fun _ _ _. have <-: f = inl_dl_hlm_gen (J i i) by apply:(inl_dl_hml_invariant iir). move => [[ff sf tf] fp]. apply:function_exten. - done. - fprops. - by aw. - by aw. - rewrite sf => x xl; rewrite idV //. move/(inductive_limit_hi): xl => [pa pb ->]. have qa: inc (J (Q (rep x)) i) (isI S). rewrite inl_dl_I ; apply/setXp_i => //. have qb: inc (P (rep x)) (Vg (isE S) (J (Q (rep x)) i)). move: pb; simpl. rewrite/inl_dl_Elam_fam LgV//. by rewrite /f inl_map_val_aux2 // /inl_dl_halm_fam LgV//; rewrite inl_prop5. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)