Changeset 1516 for src/ASM/Util.ma


Ignore:
Timestamp:
Nov 19, 2011, 12:38:20 AM (8 years ago)
Author:
sacerdot
Message:

Ported to syntax of Matita 0.99.1.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Util.ma

    r1323 r1516  
    219219    #ABSURD
    220220    elim (ABSURD nil_absurd)
    221   | normalize in cons_proof
     221  | normalize in cons_proof;
    222222    @le_S_S_to_le
    223223    assumption
     
    275275  | 3: normalize
    276276       generalize in match (sig2 … (reduce_strong A B tl tl1));
    277        >p2 >p3 >p4 normalize in ⊢ (% → ?)
     277       >p2 >p3 >p4 normalize in ⊢ (% → ?);
    278278       #HYP //
    279279  ]
     
    377377  ∀a:A.
    378378  ∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x: A.∀p:eq ? x a. P x p.
    379   #A #a #P #H #x #p
    380   generalize in match H
    381   generalize in match P
    382   cases p
    383   //
     379  #A #a #P #H #x #p lapply H lapply P cases p //
    384380qed.
    385381 
     
    400396    @ p
    401397  | 4:
    402     normalize in prf2
     398    normalize in prf2;
    403399    normalize
    404400    @ le_S_S_to_le
     
    562558 #A #B #H #acc #suff elim suff
    563559  [ #pre >append_nil %
    564   | #hd #tl #IH #pre whd in ⊢ (???%) <(foldl_step … H ??) applyS (IH (pre@[hd])) ]
     560  | #hd #tl #IH #pre whd in ⊢ (???%); <(foldl_step … H ??) applyS (IH (pre@[hd])) ]
    565561qed.
    566562
Note: See TracChangeset for help on using the changeset viewer.