Changeset 16 for Csemantics/extralib.ma
 Timestamp:
 Jul 26, 2010, 5:19:31 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Csemantics/extralib.ma
r15 r16 31 31 nlemma eq_rect_Type2_r: 32 32 ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[2]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p. 33 #A; #a; #P; #p; #x0; #p0; napply (eq_rect_r2 ??? p0); nassumption. 34 nqed. 35 36 nlemma eq_rect_CProp0_r: 37 ∀A.∀a.∀P: ∀x:A. eq ? x a → CProp[0]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p. 33 38 #A; #a; #P; #p; #x0; #p0; napply (eq_rect_r2 ??? p0); nassumption. 34 39 nqed.
Note: See TracChangeset
for help on using the changeset viewer.