fact: Fixpoint recalg_rec_type k (f : recalg k) { struct f } : P k := match f in recalg i return P i with | ra_cst n => Pcst | ra_zero => Pzero | ra_succ => Psucc | ra_proj p => Pproj p | ra_comp f gj => Pcomp [|f|] (vec_map (fun f => @recalg_rec_type _ f) gj) | ra_rec f g => Prec [|f|] [|g|] | ra_min f => Pmin [|f|] end where "[| f |]" := (@recalg_rec_type _ f).
imports: Arith Lia List Bool Eqdep_dec Undecidability.Shared.Libs.DLW(utils_tac utils_nat utils_list finite pos vec) Undecidability.MuRec.MuRec