- | @(Hlsnonulls 〈l0,false〉) >Hls @memb_hd ] ]
- | @legal_tape_conditions % % % #Hl0 >Hl0 in Hls; #Hls
- lapply (Hlsnonulls 〈null,false〉 ?)
- [ >Hls @memb_hd | normalize #H destruct (H) ]
- ]
-qed.
-
+ | @bit_not_null @(Hbits 〈l0,false〉) >Hls @memb_append_l1 @memb_hd ] ]
+ | % [ % [ %
+ [ #x #Hx cases (orb_true_l … Hx) #Hx'
+ [ >(\P Hx') %
+ | cases (memb_append … Hx') #Hx'' @Hnomarks
+ [ >Hls @memb_cons @memb_cons @(memb_append_l1 … Hx'')
+ | cases (orb_true_l … Hx'') #Hx'''
+ [ >(\P Hx''') @memb_hd
+ | @memb_cons @(memb_append_l2 … Hx''')]
+ ]
+ ]
+ | whd in ⊢ (?%); #x #Hx cases (memb_append … Hx) #Hx'
+ [ @Hbits >Hls @memb_cons @(memb_append_l1 … Hx')
+ | cases (orb_true_l … Hx') #Hx''
+ [ >(\P Hx'') //
+ | @Hbits @(memb_append_l2 … Hx'')
+ ]]]
+ | whd in ⊢ (??%?); >(Hbits 〈l0,false〉) //
+ @memb_append_l1 >Hls @memb_hd ]
+ | % % % #Hl0 lapply (Hbits 〈l0,false〉?)
+ [ @memb_append_l1 >Hls @memb_hd
+ | >Hl0 normalize #Hfalse destruct (Hfalse)
+ ] ] ] ]
+qed.
+