-| * #ta * whd in ⊢ (%→?); #Hta cases (Hta 〈mv,false〉 ?)
- [| >Hintape % ] -Hta #Hcneq cut (mv ≠ bit false)
- [ lapply (\Pf Hcneq) @not_to_not #Heq >Heq % ] -Hcneq #Hcneq #Hta destruct (Hta)
- *
- [ * #tb * whd in ⊢ (%→?);#Htb cases (Htb 〈mv,false〉 ?)
- [| >Hintape % ] -Htb #Hceq #Htb lapply (\P Hceq) -Hceq #Hceq destruct (Htb Hceq)
- * #tc * whd in ⊢ (%→?); #Htc cases (Htc … Hintape) -Htc -Hintape
- [ * normalize in ⊢ (%→?); #Hfalse destruct (Hfalse) ]
- * #_ #Htc lapply (Htc … (refl ??) (refl ??) ?)
- [ @daemon ] -Htc >append_cons <associative_append #Htc
- whd in ⊢ (%→?); #Houtc lapply (Houtc … Htc … Ht1') //
- [ >reverse_append >reverse_append >reverse_reverse @Htable
- | /2/ |]
- -Houtc -Htc * #ls1 * #rs1 * #newc * * #Houtc #Hnewtape #Hnewtapelegal
- @(ex_intro ?? ls1) @(ex_intro ?? rs1) @(ex_intro ?? newc) %
- [ //
- | %
- [ >Houtc >reverse_append >reverse_append >reverse_reverse
- >associative_append >associative_append %
- | % %2 % // ]
- ]
- | * #tb * whd in ⊢ (%→?); #Htb cases (Htb 〈mv,false〉 ?)
- [| >Hintape % ] -Htb #Hcneq' cut (mv ≠ bit true)
- [ lapply (\Pf Hcneq') @not_to_not #Heq >Heq % ] -Hcneq' #Hcneq' #Htb destruct (Htb)
- * #tc * whd in ⊢ (%→?); #Htc cases (Htc … Hintape)
- [ * >(bit_or_null_not_grid … Hmv) #Hfalse destruct (Hfalse) ] -Htc
- * #_ #Htc lapply (Htc … (refl ??) (refl ??) ?) [@daemon] -Htc #Htc
- * #td * whd in ⊢ (%→?); #Htd lapply (Htd … Htc) -Htd -Htc
- whd in ⊢ (???%→?); #Htd whd in ⊢ (%→?); #Houtc lapply (Houtc … Htd) -Houtc *
- [ * cases Htape * * #_ #_ #Hcurc #_
- >(bit_or_null_not_grid … Hcurc) #Hfalse destruct (Hfalse) ]
- * #_ #Houtc lapply (Houtc … (refl ??) (refl ??) ?) [@daemon] -Houtc #Houtc
+| * #ta * whd in ⊢ (%→?); * >Hintape #Hcneq #Hta
+ cut (mv ≠ bit false)
+ [lapply (\Pf (Hcneq … (refl …))) @not_to_not #Heq >Heq % ] -Hcneq #Hcneq
+ *
+ [* #tb * * * #ca >Hta -Hta * normalize in ⊢ (%→?); #Hdes destruct (Hdes) #eqmv
+ cut (mv = bit true) [lapply (\P eqmv) #Hdes destruct (Hdes) %] -eqmv #eqmv
+ #Htb * #tc * whd in ⊢ (%→?); #Htc cases (proj2 ?? Htc … Htb) -Htc
+ [ * >(bit_or_null_not_grid … Hmv) #Hfalse destruct (Hfalse) ]
+ * * #_ #Htc lapply (Htc ???(refl ??) (refl ??) ?)
+ [ @daemon ] -Htc >append_cons <associative_append #Htc
+ #_ whd in ⊢ (%→?); #Houtc lapply (Houtc ? n … Htc … Ht1') //
+ [ >reverse_append >reverse_append >reverse_reverse @Htable
+ | @Hmvcurc @daemon]
+ -Houtc -Htc * #ls1 * #rs1 * #newc * * #Houtc #Hnewtape #Hnewtapelegal
+ @(ex_intro ?? ls1) @(ex_intro ?? rs1) @(ex_intro ?? newc) %
+ [ //
+ | %
+ [ >Houtc >reverse_append >reverse_append >reverse_reverse
+ >associative_append >associative_append %
+ | % %2 % //
+ ]
+ ]
+ |* #tb * whd in ⊢ (%→?); * >Hta #Hcneq' #Htb
+ cut (mv ≠ bit true)
+ [lapply (\Pf (Hcneq' … (refl …))) @not_to_not #Heq >Heq % ] -Hcneq' #Hcneq'
+ * #tc * whd in ⊢ (%→?); #Htc cases (proj2 ?? Htc … Htb) -Htc
+ #_ #Htc cases (Htc (bit_or_null_not_grid … Hmv)) -Htc #Htc #_
+ lapply (Htc … (refl ??) (refl ??) ?) [@daemon] -Htc #Htc
+ * #td * whd in ⊢ (%→?); #Htd lapply (proj2 ?? Htd … Htc) -Htd -Htc
+ whd in ⊢ (???%→?); #Htd whd in ⊢ (%→?); #Houtc cases (proj2 ?? Houtc … Htd)
+ -Houtc #_ #Houtc cases (Houtc ?)
+ [2: cases Htape * * #_ #_ #Hcurc #_ >(bit_or_null_not_grid … Hcurc) %]
+ #Houtc #_ lapply (Houtc … (refl ??) (refl ??) ?) [@daemon] -Houtc #Houtc