Changeset 1351 for src/utilities/deppair.ma
 Timestamp:
 Oct 11, 2011, 12:24:33 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/utilities/deppair.ma
r1316 r1351 1 (* TODO: merge with utilities/sigma.ma *) 2 1 3 include "ASM/JMCoercions.ma". (* This contains rather more than we really want. *) 2 4 … … 7 9 #A #P * #a #p @p 8 10 qed. 11 12 lemma 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 14 qed.
Note: See TracChangeset
for help on using the changeset viewer.