diff options
Diffstat (limited to 'theories/Logic/EqdepFacts.v')
| -rw-r--r-- | theories/Logic/EqdepFacts.v | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/theories/Logic/EqdepFacts.v b/theories/Logic/EqdepFacts.v index 8e59941f37..b930388d13 100644 --- a/theories/Logic/EqdepFacts.v +++ b/theories/Logic/EqdepFacts.v @@ -372,8 +372,7 @@ Proof. rewrite (UIP_refl y). intros z. assert (UIP:forall y' y'' : x = x, y' = y''). - { intros. apply eq_trans with (eq_refl x). apply UIP_refl. - symmetry. apply UIP_refl. } + { intros. apply eq_trans_r with (eq_refl x); apply UIP_refl. } transitivity (eq_trans (eq_trans (UIP (eq_refl x) (eq_refl x)) z) (eq_sym (UIP (eq_refl x) (eq_refl x)))). - destruct z. destruct (UIP _ _). reflexivity. |