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/List.ma

    r350 r352  
    236236    ##|##3:
    237237        nnormalize in prf;
    238         ndestruct (prf);
    239         nassumption;
     238        nlapply (S_inj … prf);
     239        #X; nrewrite > X; @;
    240240    ##]
    241241nqed.
Note: See TracChangeset for help on using the changeset viewer.