Ignore:
Timestamp:
Jun 21, 2012, 5:21:03 PM (9 years ago)
Author:
campbell
Message:

Fill in misc axiom.

File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/common/PositiveMap.ma

    r1882 r2104  
    7777] qed.
    7878
    79 axiom lookup_insert_hit:
     79lemma lookup_insert_hit:
    8080  ∀a: Type[0].
    8181  ∀v: a.
    … …  
    8484  ∀d: a.
    8585    lookup … b (insert … b v t) d = v.
     86#A #v #b #t #d whd in ⊢ (??%?); >lookup_opt_insert_hit %
     87qed.
    8688
    8789lemma lookup_opt_insert_miss:
Note: See TracChangeset for help on using the changeset viewer.