- #l1;
- napply (list_ind ascii ??? l1);
- ##[ ##1: #l2; ncases l2;
- ##[ ##1: nnormalize; #H; napply (refl_eq ??)
- ##| ##2: #x1; #x2; nnormalize; #H; nelim (list_destruct_nil_cons ascii ?? H)
- ##]
- ##| ##2: #x1; #x2; #H; #l2; ncases l2;
- ##[ ##1: #H; nelim (list_destruct_cons_nil ascii ?? H)
- ##| ##2: #y1; #y2; #H1;
- nrewrite > (list_destruct_1 ascii ???? H1);
- nchange with (((eq_ascii y1 y1)⊗(eq_str x2 y2)) = true);
- nrewrite > (H y2 (list_destruct_2 ascii ???? H1));
- nrewrite > (eq_to_eqascii y1 y1 (refl_eq ??));
- nnormalize;
- napply (refl_eq ??)
- ##]
- ##]