bug_13456.v « closed « bugs « test-suite - coq - The formal proof system

about summary refs log tree commit diff

path: root/test-suite/bugs/closed/bug_13456.v

blob: b2e7fa7be573add9607386196a87dab76f99f3df (plain)

Lemma minbug (n : nat) (P : nat -> Prop) (pn : P n) : exists (m : nat) (p : P m), True.
Proof.
  exists _, pn.
  exact I.
Qed.