Changeset 2226 for src/common
- Timestamp:
- Jul 20, 2012, 6:36:34 PM (7 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/common/Globalenvs.ma
r2185 r2226 548 548 ] 549 549 ] qed. 550 551 (* lazy proof *) 552 lemma find_funct_ptr_All : ∀A,V,b,p,f,initV,P. 553 find_funct_ptr … (globalenv A V initV p) b = Some ? f → 554 All ? (λx. P (\snd x)) (prog_funct ?? p) → 555 P f. 556 #A #V #b #p #f #initV #P #FFP #ALL 557 cut (All2 ?? (λx,y. P (\snd x)) (prog_funct ?? p) (prog_funct ?? p)) 558 [ elim (prog_funct … p) in ALL ⊢ %; 559 [ // | #h #t #IH * #Hh #Ht % /2/ ] ] 560 #ALL2 561 cases (find_funct_ptr_All2 A A V V b p f initV initV p ? FFP ALL2) 562 #x * // 563 qed. 564 550 565 551 566 discriminator Prod.
Note: See TracChangeset
for help on using the changeset viewer.