fact: Definition dest_pair {T} (x:T) : M (dyn * dyn) := mmatch Dyn x with | [? A B a b] @Dyn (A*B) (a, b) => ret (Dyn a, Dyn b) end.
imports: Mtac2(Base Datatypes List MTele MTeleMatch MTeleMatchDef MFixDef Sorts tactics.Tactics) Strings.String