fact: Fixpoint get_ATele {isort} (it : ITele isort) (al : mlist dyn) {struct al} : M (ATele it) := match it as it', al return M (ATele it') with | iBase T, [m:] => M.ret tt | iTele f, t_dyn :m: al => dcase t_dyn as el in t <- M.coerce el; r <- get_ATele (f t) al; M.ret (existT _ t r) | _, _ => M.raise NoPatternMatches end.
imports: Mtac2(Logic Datatypes List Sorts Base MTeleMatch MFix) Mtac2.tactics(Tactics ImportedTactics) Strings.String