source:
Deliverables/D3.3/id-lookup-branch/utilities/deppair.ma
Last change on this file 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.