+ |cases HPre -HPre #ls * #c * #c0 * #rs * #l1 * #l3 * #l4
+ * * * * * #Ht #Hl1nomarks #Hl3l4nomarks #Hlen
+ * #l1' * #bv * #Hl1 #Hbitsnullsl1'
+ * #l4' * #bg * #Hl4 #Hbitsnullsl4'
+ >Ht lapply Hbitsnullsl1' lapply Hl1 lapply l1' lapply Hl3l4nomarks
+ lapply Hl1nomarks lapply l3 lapply c0 lapply c lapply ls
+ -Hbitsnullsl1' -Hl1 -l1' -Hl3l4nomarks -Hl1nomarks -l3 -Hl4 -c0 -c -ls
+ <(reverse_reverse ? l4) <(length_reverse ? l4) in Hlen; #Hlen
+ @(list_ind2 … Hlen)
+ [ #ls #c #c0 #l3 #_ #_ #l1' #Hl1 #Hbitsnullsl1' cases l1' in Hl1;
+ [| #x * [| #x0 #xs ] normalize in ⊢ (%→?); #Hfalse destruct (Hfalse) ]
+ normalize in ⊢ (%→?); #Hl1' destruct (Hl1') % #t1 whd in ⊢ (%→?);
+ #HR cases (HR … (refl …)) whd in ⊢ (??%?→?); #Hfalse destruct (Hfalse)
+ | #xs #ys * #x #bx * #y #by #IH
+ #ls #c #c0 #l3 #Hl1nomarks #Hl3l4nomarks #l1' #Hl1
+ #Hbitsnullsl1' %
+ #t1 whd in ⊢ (%→?); #HR cases (HR … (refl …)) -HR
+ #Hbitnullc #HR
+ lapply (Hl1nomarks 〈x,bx〉 (memb_hd …)) normalize in ⊢ (%→?); #Hbx destruct (Hbx)
+ (*cut (∃d2,l4''.〈y,by〉::ys = l4''@[〈d2,false〉])
+ [ cases (list_last ? ys) in Hl3l4nomarks;
+ [ #Hl4' #Hl3l4nomarks >Hl4' >(?:by = false) [%{y} %{([])} %]
+ @(Hl3l4nomarks 〈y,by〉) @memb_append_l2 @memb_hd
+ | * * #d2 #bd2 * #l4'' #Hl4'' >Hl4'' #Hl3l4nomarks
+ <(?:bd2 = false) [| @(Hl3l4nomarks 〈d2,bd2〉) @memb_append_l2 @memb_cons @memb_append_l2 @memb_hd ]
+ %{d2} %{(〈y,by〉::l4'')} % ] ]
+ * #a0 * #l4'' #Hl4'' >Hl4'' in HR; #HR *)
+ cases (HR x (l3@reverse ? ys) c0 y ls (xs@rs) ? (refl …) ?)
+ [3: >reverse_cons >associative_append >associative_append
+ >(?:by = false) [|@(Hl3l4nomarks 〈y,by〉) @memb_append_l2 >reverse_cons @memb_append_l2 @memb_hd ] %
+ |4: #x #Hx @Hl3l4nomarks >reverse_cons <associative_append @memb_append_l1 @Hx
+ | * #x1 * #Hc #Ht1 >Ht1
+ <(?: (〈bit x1,false〉::l3)@reverse (FSUnialpha×bool) ys@〈y,true〉::〈bit x1,false〉::ls =
+ 〈bit x1,false〉::(l3@reverse (FSUnialpha×bool) ys)@〈y,true〉::〈bit x1,false〉::ls)
+ [cut (∃l1''.〈x,false〉::xs = l1''@[〈comma,bv〉] ∧ only_bits_or_nulls l1'')
+ [lapply Hbitsnullsl1' lapply Hl1 -Hl1 -Hbitsnullsl1' cases l1'
+ [normalize in ⊢(%→?); #Hfalse destruct (Hfalse)
+ |#x2 #l1'' normalize in ⊢ (%→?); #Heq #Hbitsnullsl1' destruct (Heq)
+ %{l1''} % [@e0]
+ #x #Hx @Hbitsnullsl1' @memb_cons @Hx ] ]
+ * #l1'' * #Hl1'' #Hbitsnullsl1''
+ @(IH (〈bit x1,false〉::ls) x y (〈bit x1,false〉::l3) ?? l1'' Hl1'' Hbitsnullsl1'')
+ [#x #Hx @Hl1nomarks @memb_cons @Hx
+ |#x #Hx cases (orb_true_l … Hx) -Hx #Hx
+ [>(\P Hx) %
+ |cases (memb_append … Hx) -Hx #Hx @Hl3l4nomarks
+ [@memb_append_l1 @Hx
+ |@memb_append_l2 >reverse_cons @memb_append_l1 @Hx ] ] ]
+ |>associative_append % ]
+ | * #Hc #Ht1 >Ht1
+ <(?: (〈null,false〉::l3)@reverse (FSUnialpha×bool) ys@〈y,true〉::〈c0,false〉::ls =
+ 〈null,false〉::(l3@reverse (FSUnialpha×bool) ys)@〈y,true〉::〈c0,false〉::ls)
+ [cut (∃l1''.〈x,false〉::xs = l1''@[〈comma,bv〉] ∧ only_bits_or_nulls l1'')
+ [lapply Hbitsnullsl1' lapply Hl1 -Hl1 -Hbitsnullsl1' cases l1'
+ [normalize in ⊢(%→?); #Hfalse destruct (Hfalse)
+ |#x2 #l1'' normalize in ⊢ (%→?); #Heq #Hbitsnullsl1' destruct (Heq)
+ %{l1''} % [@e0]
+ #x #Hx @Hbitsnullsl1' @memb_cons @Hx ] ]
+ * #l1'' * #Hl1'' #Hbitsnullsl1''
+ @(IH (〈c0,false〉::ls) x y (〈null,false〉::l3) ?? l1'' Hl1'' Hbitsnullsl1'')
+ [#x #Hx @Hl1nomarks @memb_cons @Hx
+ |#x #Hx cases (orb_true_l … Hx) -Hx #Hx
+ [>(\P Hx) %
+ |cases (memb_append … Hx) -Hx #Hx @Hl3l4nomarks
+ [@memb_append_l1 @Hx
+ |@memb_append_l2 >reverse_cons @memb_append_l1 @Hx ] ] ]
+ |>associative_append % ]
+]]]