diff options
author | Abhishek Anand <abhishek.anand.iitg@gmail.com> | 2016-12-11 11:59:33 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2016-12-11 11:59:33 -0500 |
commit | d7abadbef61ab0d45ffc5a5a45ff31bd39103446 (patch) | |
tree | 37f13e8e56641a432b105a92578ed526d8d4d614 /plugins/ltac | |
parent | ad768e435a736ca51ac79a575967b388b34918c7 (diff) |
strengthened the statement of JMeq_eq_dep
because P:U->Prop implies P:U->Type, the new statement is strictly more useful.
No change was needed to the proof.
Diffstat (limited to 'plugins/ltac')
0 files changed, 0 insertions, 0 deletions