Ignore:
Timestamp:
Mar 7, 2013, 1:29:31 PM (7 years ago)
Author:
piccolo
Message:

Partial commit not yet finished

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/ExtraIdentifiers.ma

    r2783 r2801  
    235235
    236236
    237 
    238 
     237lemma empty_set_minus : ∀tag,A,B.∀m : identifier_map tag B. empty_map tag A =
     238empty_map tag A ∖ m.
     239#tag #A #B * #m normalize @eq_f elim m [%] #opt_b #l #r #IHl #IHr normalize
     240cases opt_b normalize [2: #b] <IHl <IHr %
     241qed.
     242
     243
Note: See TracChangeset for help on using the changeset viewer.