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