Changeset 328 for Deliverables/D4.1/Matita/Plogic
 Timestamp:
 Nov 29, 2010, 11:17:58 AM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/Plogic/equality.ma
r268 r328 32 32 ∀A.∀a.∀P: ∀x:A. x = a → Prop. P a (refl A a) → ∀x.∀p:eq ? x a.P x p. 33 33 #A; #a; #P; #p; #x0; #p0; napply (eq_rect_r ? ? ? p0); nassumption. 34 nqed. 35 36 nlemma eq_rect_Type0_r : 37 ∀A: Type[0]. 38 ∀a:A. 39 ∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x: A.∀p:eq ? x a. P x p. 40 #A a P H x p. 41 ngeneralize in match H. 42 ngeneralize in match P. 43 ncases p. 44 //. 34 45 nqed. 35 46
Note: See TracChangeset
for help on using the changeset viewer.