Ignore:
Timestamp:
Aug 30, 2012, 4:47:58 PM (8 years ago)
Author:
campbell
Message:

Half the proofs for sound cost labelling check.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Identifiers.ma

    r2305 r2307  
    979979* #_ #H @H
    980980qed.
     981
     982lemma try_remove_this : ∀tag,A,m,id,a.
     983  lookup tag A m id = Some A a →
     984  ∃m'. try_remove tag A m id = Some ? 〈a,m'〉.
     985#tag #A * #m * #id #a #L
     986cases (pm_try_remove_some' A id m a L)
     987#m' #R %{(an_id_map tag A m')} whd in ⊢ (??%?); >R %
     988qed.
    981989 
    982990
Note: See TracChangeset for help on using the changeset viewer.