Ignore:
Timestamp:
Oct 11, 2011, 12:24:33 PM (8 years ago)
Author:
campbell
Message:

Tidy up some loose ends from the invariants branch merge.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/deppair.ma

    r1316 r1351  
     1(* TODO: merge with utilities/sigma.ma *)
     2
    13include "ASM/JMCoercions.ma". (* This contains rather more than we really want. *)
    24
     
    79#A #P * #a #p @p
    810qed.
     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 TracChangeset for help on using the changeset viewer.