source: Deliverables/D3.3/id-lookup-branch/utilities/deppair.ma @ 1133

Last change on this file since 1133 was 1133, checked in by campbell, 8 years ago

Add missing utilities files

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.