fact: Fixpoint Mnth (n:nat) (l:metalist) (default:A) {struct l} : A := match n, l with | O, Mcons x l' => x | O, other => default | S m, Mnil => default | S m, Mcons x t => Mnth m t default end.
imports: CoRN.logic.CLogic Coq.Bool.Bool