4325.v « closed « bugs « test-suite - debian-coq - Debian packaging for Coq

summary refs log tree commit diff

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

blob: af69ca04b6cd82e3acf573445b8ff7a72848540d (plain)

Goal (forall a b : nat, Set = (a = b)) -> Set.
Proof.
  clear.
  intro H.
  erewrite (fun H' => H _ H').