Changeset 873 for src

Timestamp:

Jun 2, 2011, 5:47:00 PM (9 years ago)

Author:

sacerdot

Message:

Script improved. Maybe this requires an svn up of Matita.

File:

• src/ASM/Vector.ma (modified) (2 diffs)

src/ASM/Vector.ma

@@ -117 +117 @@
     /2/;
 qed.
-    
+
 let rec set_index_weak (A: Type[0]) (n: nat)
                        (v: Vector A n) (m: nat) (a: A) on m ≝
@@ -457 +457 @@
   | S m ⇒ λP.λv.(∀h,t. P (VCons A m h t)) → P v
   ] P v.
-@(λA,n. λP:Vector A n → Type[0]. λv. match v return
-?
-with [ VEmpty ⇒ ? | VCons m h t ⇒ ? ] P)
-[ // | // ] qed.
-(* XXX Proof below fails at qed.
-#A #n #P * [ #H @H | #m #h #t #H @H ] qed.
-*)
+#A #n #P #v generalize in match P cases v normalize //
+qed.
 
 lemma eq_v_elim: ∀P:bool → Type[0]. ∀A,f.