source:
src/utilities/deppair.ma
@
1330
Last change on this file since 1330 was 1316, checked in by , 9 years ago | |
---|---|
File size: 269 bytes |
Rev | Line | |
---|---|---|
[1133] | 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.