Changeset 2307 for src/common/PositiveMap.ma
- Timestamp:
- Aug 30, 2012, 4:47:58 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/common/PositiveMap.ma
r2305 r2307 548 548 ] qed. 549 549 550 551 550 lemma pm_try_remove_some' : ∀A,p,t,a. 551 lookup_opt A p t = Some A a → 552 ∃t'. pm_try_remove A p t = Some ? 〈a,t'〉. 553 #A #p elim p 554 [ * [ #a #L normalize in L; destruct 555 | #q #l #r #a #L normalize in L; destruct % [2: % | skip ] 556 ] 557 | #q #IH * 558 [ #a #L normalize in L; destruct 559 | #x #l #r #a #L cases (IH r a L) #r' #R 560 % [2: whd in ⊢ (??%?); >R in ⊢ (??%?); % | skip ] 561 ] 562 | #q #IH * 563 [ #a #L normalize in L; destruct 564 | #x #l #r #a #L cases (IH l a L) #l' #R 565 % [2: whd in ⊢ (??%?); >R in ⊢ (??%?); % | skip ] 566 ] 567 ] qed. 568 569
Note: See TracChangeset
for help on using the changeset viewer.