fact: Fixpoint combine {A B} (l : mlist A) (l' : mlist B) {struct l} : mlist (A *m B) := match l with | mnil => mnil | (x :m: tl)%list => match l' with | mnil => mnil | (y :m: tl')%list => ((m: x, y) :m: combine tl tl')%list end end.
imports: Coq.Strings.String Mtac2(Base Logic Datatypes List Sorts DepDestruct MTeleMatch)