Ignore:
Timestamp:
Dec 1, 2010, 6:03:45 PM (9 years ago)
Author:
mulligan
Message:

Do not use ndestruct for injectivity since it introduces StreickerK that
blocks reductions.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/Matita/Status.ma

    r351 r352  
    893893 nelim n in ⊢ (∀_:?. ??% → ?(?%??)?)
    894894  [ nnormalize; #n; napply (less_than_or_equal_b_elim n m); nnormalize
    895      [ // | #H K; ninversion K [ #H1; ndestruct; // | #x H1 H2 H3; ndestruct ]##]
     895     [ // | #H K; ninversion K [ #H1; nrewrite < H1; // | #x H1 H2 H3; ndestruct ]##]
    896896##| nnormalize; #y H1 n H2; napply (less_than_or_equal_b_elim n m); nnormalize
    897897     [ // | #K; napply H1; ncut (n ≤ S y → n - S m ≤ y); /2/;
Note: See TracChangeset for help on using the changeset viewer.