fact: Example reflect_itele : ITele reflect_sort := Eval compute in match msnd get_reflect_ITele as pair return let (sort, _) := pair in ITele sort with | existT _ s it => it end.
imports: Mtac2(Datatypes List Mtac2 DepDestruct Sorts MTeleMatch)