fact: Definition compi {A} {B} (g : M A) (h : M B) : M (A * B) := g >>= fun xg=> h >>= fun xh => ret (xg, xh).
imports: Mtac2(Base Datatypes List MTele MTeleMatch MTeleMatchDef MFixDef Sorts tactics.Tactics) Strings.String