Changeset 328 for Deliverables/D4.1/Matita/Plogic

Timestamp:

Nov 29, 2010, 11:17:58 AM (10 years ago)

Author:

mulligan

Message:

Got fold_right_i to type check. Moved eq_rect_Type0 into Plogic/equality.ma. Added new file for main processor execution loop.

File:

• Deliverables/D4.1/Matita/Plogic/equality.ma (modified) (1 diff)

Deliverables/D4.1/Matita/Plogic/equality.ma

@@ -32 +32 @@
  ∀A.∀a.∀P: ∀x:A. x = a → Prop. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
  #A; #a; #P; #p; #x0; #p0; napply (eq_rect_r ? ? ? p0); nassumption.
+nqed.
+
+nlemma eq_rect_Type0_r :
+  ∀A: Type[0].
+  ∀a:A.
+  ∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x: A.∀p:eq ? x a. P x p.
+  #A a P H x p.
+  ngeneralize in match H.
+  ngeneralize in match P.
+  ncases p.
+  //.
 nqed.