Ignore:
Timestamp:
Dec 13, 2011, 1:34:37 AM (8 years ago)
Author:
sacerdot
Message:

Start of merging of stuff into the standard library of Matita.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/TranslateUtils.ma

    r1521 r1599  
    2121 #pars0 #globals #def #n elim n
    2222  [ %
    23   | #m whd in ⊢ (? → ??(??%)?); whd in ⊢ (? → ??(??match % with [ _ ⇒ ?])?) ;
    24     cases (fresh_regs pars0 globals def m) normalize nodelta
    25     #def' #regs #EQ change with (|regs| = m)in EQ; <EQ
    26     @refl
    27  ]
     23  | #m whd in ⊢ (? → ??(??(???%))?); @pair_elim
     24    #def' #regs #EQ >EQ  normalize // ]
    2825qed.
    2926
Note: See TracChangeset for help on using the changeset viewer.