diff options
Diffstat (limited to 'theories/Logic')
| -rw-r--r-- | theories/Logic/JMeq.v | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/theories/Logic/JMeq.v b/theories/Logic/JMeq.v index f17e403ed9..330ee79efd 100644 --- a/theories/Logic/JMeq.v +++ b/theories/Logic/JMeq.v @@ -111,8 +111,7 @@ apply JMeq_refl. Qed. Lemma eq_dep_strictly_stronger_JMeq : - exists U, exists P, exists p, exists q, exists x, exists y, - JMeq x y /\ ~ eq_dep U P p x q y. + exists U P p q x y, JMeq x y /\ ~ eq_dep U P p x q y. Proof. exists bool. exists (fun _ => True). exists true. exists false. exists I. exists I. |