test-suite/bugs/closed/bug_sprop_13.v


1
2
3
4
5
6
7

(* -*- mode: coq; coq-prog-args: ("-allow-sprop") -*- *)
Goal forall (P : SProp), P -> P.
Proof.
  intros P H. set (H0 := H).
  (* goal is now H0 *)
  exact H0.
Qed.