nlemma eq_rect_CProp0_r:
∀A.∀a.∀P: ∀x:A. eq ? x a → CProp[0]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
- #A; #a; #x; #p; #x0; #p0; napply eq_rect_CProp0_r'; nassumption.
+ #A; #a; #P; #p; #x0; #p0; napply (eq_rect_CProp0_r' ??? p0); nassumption.
nqed.
interpretation "leibnitz's equality" 'eq t x y = (eq t x y).