-(*
+ (*
||M|| This file is part of HELM, an Hypertextual, Electronic
||A|| Library of Mathematics, developed at the Computer Science
||T|| Department of the University of Bologna, Italy.
lemma eq_rect_Type0_r:
∀A.∀a.∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
- #A #a #P #H #x #p (generalize in match H) (generalize in match P)
+ #A #a #P #H #x #p (generalize {match H}) (generalize {match P})
cases p; //; qed.
-
+
+lemma eq_rect_Type1_r:
+ ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[1]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
+ #A #a #P #H #x #p (generalize {match H}) (generalize {match P})
+ cases p; //; qed.
+
lemma eq_rect_Type2_r:
∀A.∀a.∀P: ∀x:A. eq ? x a → Type[2]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
- #A #a #P #H #x #p (generalize in match H) (generalize in match P)
+ #A #a #P #H #x #p (generalize {match H}) (generalize {match P})
cases p; //; qed.
lemma eq_rect_Type3_r:
∀A.∀a.∀P: ∀x:A. eq ? x a → Type[3]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
- #A #a #P #H #x #p (generalize in match H) (generalize in match P)
+ #A #a #P #H #x #p (generalize {match H}) (generalize {match P})
cases p; //; qed.
theorem rewrite_l: ∀A:Type[2].∀x.∀P:A → Type[2]. P x → ∀y. x = y → P y.
#A #x #P #Hx #y #Heq (cases Heq); //; qed.
theorem sym_eq: ∀A.∀x,y:A. x = y → y = x.
-#A #x #y #Heq @(rewrite_l A x (λz.z=x)); //; qed.
+#A #x #y #Heq @(rewrite_l A x (λz.z=x)) // qed.
theorem rewrite_r: ∀A:Type[2].∀x.∀P:A → Type[2]. P x → ∀y. y = x → P y.
#A #x #P #Hx #y #Heq (cases (sym_eq ? ? ? Heq)); //; qed.