-[ * #ta * whd in ⊢ (%→?); >Hintape #Hta cases (Hta … (refl ??)) -Hta #Hx #Hta
- * #tb * whd in ⊢ (%→?); #Htb lapply (Htb … Hta) -Hta -Htb #Htb
- * #tc * whd in ⊢ (%→?); #Htc lapply (Htc … Htb) -Htb -Htc #Htc
- * #td * whd in ⊢ (%→?); #Htd cases (Htd … Htc) -Htd
- [ >Htc * normalize in ⊢ (%→?); #Hfalse destruct (Hfalse) ]
- * #_ #Htd lapply (Htd (l1@[〈a0,false〉]) 〈x0,true〉 l2 ? (refl ??) ?) -Htd
- [ #x1 #Hx1 cases (memb_append … Hx1) -Hx1 #Hx1 [@(Hl1marks ? Hx1)|>(memb_single … Hx1) %]
- | normalize >associative_append % ] >reverse_append #Htd
- * #te * whd in ⊢ (%→?); #Hte lapply (Hte … Htd) -Hte -Htd -Htc #Hte
- * #tf * whd in ⊢ (%→?); #Htf lapply (Htf … Hte) -Hte -Htf
+[ * #ta * whd in ⊢ (%→?); >Hintape * * #c * whd in ⊢ (??%?→?); #Hc destruct (Hc) #Hx #Hta
+ * #tb * whd in ⊢ (%→?); * #Htb #_ cases (Htb (l1@〈a0,false〉::〈x0,true〉::l2) x) -Htb #Htb #_ lapply (Htb … Hta) -Hta -Htb #Htb
+ * #tc * whd in ⊢ (%→?); * #_ #Htc lapply (Htc … Htb) -Htb -Htc #Htc
+ * #td * whd in ⊢ (%→?); * #_ #Htd cases (Htd … Htc) -Htd #_ #Htd cases (Htd (refl …)) -Htd #Htd #_
+ lapply (Htd (l1@[〈a0,false〉]) 〈x0,true〉 l2 ? (refl …) ?)
+ [#x1 #Hx1 cases (memb_append … Hx1) [@Hl1marks| -Hx1 #Hx1 >(memb_single … Hx1) % ]
+ |>associative_append % ] -Htd >reverse_append in ⊢ (???%→?); >associative_append in ⊢ (???%→?); #Htd
+ * #te * whd in ⊢ (%→?); * #Hte cases (Hte l2 x0) -Hte #Hte #_ #_ lapply (Hte … Htd) -Hte -Htd -Htc #Hte
+ * #tf * whd in ⊢ (%→?); * #_ #Htf lapply (Htf … Hte) -Hte -Htf