nelim b2;
nnormalize;
#H;
- ##[ ##2: napply (False_ind (λx.?) ?);
+ ##[ ##2: napply False_ind;
nchange with (match true with [ true ⇒ False | false ⇒ True]);
nrewrite > H;
nnormalize;
napply I
- ##| ##3: napply (False_ind (λx.?) ?);
+ ##| ##3: napply False_ind;
nchange with (match true with [ true ⇒ False | false ⇒ True]);
nrewrite < H;
nnormalize;