- ##[ ##1: nelim m2; nnormalize; #H;
- ##[ ##1: napply (λx:P.x)
- ##| ##*: napply (False_ind ??);
- nchange with (match HC05 with [ HC05 ⇒ False | _ ⇒ True ]);
- nrewrite > H; nnormalize; napply I
- ##]
- ##| ##2: nelim m2; nnormalize; #H;
- ##[ ##2: napply (λx:P.x)
- ##| ##*: napply (False_ind ??);
- nchange with (match HC08 with [ HC08 ⇒ False | _ ⇒ True ]);
- nrewrite > H; nnormalize; napply I
- ##]
- ##| ##3: nelim m2; nnormalize; #H;
- ##[ ##3: napply (λx:P.x)
- ##| ##*: napply (False_ind ??);
- nchange with (match HCS08 with [ HCS08 ⇒ False | _ ⇒ True ]);
- nrewrite > H; nnormalize; napply I
- ##]
- ##| ##4: nelim m2; nnormalize; #H;
- ##[ ##4: napply (λx:P.x)
- ##| ##*: napply (False_ind ??);
- nchange with (match RS08 with [ RS08 ⇒ False | _ ⇒ True ]);
- nrewrite > H; nnormalize; napply I
- ##]
- ##]