diff options
| -rw-r--r-- | theories/Init/Logic.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index 85123cc444..504ef95d98 100644 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -553,7 +553,8 @@ Proof. intros A P (x & Hp & Huniq); split. - intro; exists x; auto. - intros (x0 & HPx0 & HQx0) x1 HPx1. - replace x1 with x0 by (transitivity x; [symmetry|]; auto). + assert (H : x0 = x1) by (transitivity x; [symmetry|]; auto). + destruct H. assumption. Qed. |