test-suite/bugs/closed/3010b.v


1
2
3
4
5

Definition wtf (n : nat) : nat :=
  (match n with
       0 => (fun H : n = 0 => 0)
     | S n' => (fun H : n = S n' => 0)
   end) (eq_refl n).