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

    r351 r352  
    1313  Z: Nat
    1414| S: Nat → Nat.
     15
     16ntheorem S_inj: ∀n,m:Nat. S n = S m → n=m.
     17 #n m H;
     18 nchange with (n = match S m with [ Z ⇒ Z | S x ⇒ x]);
     19 napply (match H return λx.λ_. n = match x with [Z ⇒ Z | S x ⇒ x] with [ refl ⇒ ? ]);
     20 nnormalize; /3/.
     21nqed.
    1522
    1623(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    606613 #m; nelim m; nnormalize
    607614  [ #n H; ndestruct | #y H1 z; ncases z; nnormalize
    608     [ #H; ndestruct | /3/ ] /2/.
     615    [ #H; /2/ | /3/ ]
    609616nqed.
    610617
Note: See TracChangeset for help on using the changeset viewer.