source: src/utilities/deppair.ma @ 1341

Last change on this file since 1341 was 1316, checked in by campbell, 9 years ago

Merge in id-lookup-branch to trunk.

File size: 269 bytes
Line 
1include "ASM/JMCoercions.ma". (* This contains rather more than we really want. *)
2
3notation "hvbox(« term 19 a, break term 19 b»)"
4with precedence 90 for @{ (dp ?? $a $b) }.
5
6lemma use_sig : ∀A:Type[0]. ∀P:A → Prop. ∀x:Σx:A.P x. P x.
7#A #P * #a #p @p
8qed.
Note: See TracBrowser for help on using the repository browser.