Changeset 1516 for src/ASM/Util.ma

Timestamp:

Nov 19, 2011, 12:38:20 AM (8 years ago)

Author:

sacerdot

Message:

Ported to syntax of Matita 0.99.1.

File:

• src/ASM/Util.ma (modified) (5 diffs)

src/ASM/Util.ma

@@ -219 +219 @@
     #ABSURD
     elim (ABSURD nil_absurd)
-  | normalize in cons_proof
+  | normalize in cons_proof;
     @le_S_S_to_le
     assumption
@@ -275 +275 @@
   | 3: normalize
        generalize in match (sig2 … (reduce_strong A B tl tl1));
-       >p2 >p3 >p4 normalize in ⊢ (% → ?)
+       >p2 >p3 >p4 normalize in ⊢ (% → ?);
        #HYP //
   ]
@@ -377 +377 @@
   ∀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
-  generalize in match H
-  generalize in match P
-  cases p
-  //
+  #A #a #P #H #x #p lapply H lapply P cases p //
 qed.
   
@@ -400 +396 @@
     @ p
   | 4:
-    normalize in prf2
+    normalize in prf2;
     normalize
     @ le_S_S_to_le
@@ -562 +558 @@
  #A #B #H #acc #suff elim suff
   [ #pre >append_nil %
-  | #hd #tl #IH #pre whd in ⊢ (???%) <(foldl_step … H ??) applyS (IH (pre@[hd])) ] 
+  | #hd #tl #IH #pre whd in ⊢ (???%); <(foldl_step … H ??) applyS (IH (pre@[hd])) ] 
 qed.