fact: Fixpoint nth_bad (l:natlist) (n:nat) : nat := match l with | nil => 42 | a :: l' => match beq_nat n O with | true => a | false => nth_bad l' (pred n) end end.
imports: QuickChick(QuickChick) List ZArith Induction