Changeset 2226 for src/common
 Timestamp:
 Jul 20, 2012, 6:36:34 PM (9 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.