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 |
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.