- [##1,8: #_; #K; (* non va ndestruct K; *) ncases (?:⊥); (* perche' due goal?*) /2/
- |##2,9: #X; #Y; #K; ncases (?:⊥); /2/
- |##3,10: #x; #y; #z; #w; #a; #b; #c; #d; #e; #K; ncases (?:⊥); /2/
- |##4,11: #x; #y; #z; #w; #a; #b; #K; ncases (?:⊥); /2/
- |##5,12: #x; #y; #z; #w; #a; #b; #K; ncases (?:⊥); /2/
- |##6,13: #x; #y; #K; ncases (?:⊥); /2/
- |##7,14: #x; #y; #z; #w; #a; #b; #c; #d; #K; ncases (?:⊥); /2/]
+ [##1,8: #_; #K; (* non va ndestruct K; *) ncases (?:False); (* perche' due goal?*) /2/
+ |##2,9: #X; #Y; #K; ncases (?:False); /2/
+ |##3,10: #x; #y; #z; #w; #a; #b; #c; #d; #e; #K; ncases (?:False); /2/
+ |##4,11: #x; #y; #z; #w; #a; #b; #K; ncases (?:False); /2/
+ |##5,12: #x; #y; #z; #w; #a; #b; #K; ncases (?:False); /2/
+ |##6,13: #x; #y; #K; ncases (?:False); /2/
+ |##7,14: #x; #y; #z; #w; #a; #b; #c; #d; #K; ncases (?:False); /2/]