source: src/utilities/deppair.ma @ 1415

Last change on this file since 1415 was 1351, checked in by campbell, 9 years ago

Tidy up some loose ends from the invariants branch merge.

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