fact: Fixpoint mnth {A} (n:nat) (l:mlist A) (default:A) {struct l} : A := match n, l with | O, x :m: l' => x | O, other => default | S m, [m:] => default | S m, x :m: t => mnth m t default end.
imports: Mtac2.lib.Datatypes