source:
Deliverables/D3.3/id-lookup-branch/utilities/deppair.ma
@
2113
| Last change on this file since 2113 was 1133, checked in by , 9 years ago | |
|---|---|
| File size: 269 bytes | |
| Line | |
|---|---|
| 1 | include "ASM/JMCoercions.ma". (* This contains rather more than we really want. *) |
| 2 | |
| 3 | notation "hvbox(« term 19 a, break term 19 b»)" |
| 4 | with precedence 90 for @{ (dp ?? $a $b) }. |
| 5 | |
| 6 | lemma use_sig : ∀A:Type[0]. ∀P:A → Prop. ∀x:Σx:A.P x. P x. |
| 7 | #A #P * #a #p @p |
| 8 | qed. |
Note: See TracBrowser
for help on using the repository browser.
