+ only_bits (l4@[〈s0,false〉]) → only_bits (〈s1,false〉::l1) →
+ bit_or_null c0 = true → bit_or_null c1 = true →
+ t2 = midtape STape (〈c1,false〉::reverse ? l1@〈s1,false〉::l3@〈grid,false〉::
+ 〈merge_char c0 c1,false〉::reverse ? l1@〈s1,false〉::ls)
+ 〈comma,false〉 rs.
+
+axiom sem_copy0 : Realize ? copy0 R_copy0.
+
+definition option_cons ≝ λA.λa:option A.λl.
+ match a with
+ [ None ⇒ l
+ | Some a' ⇒ a'::l ].
+
+lemma sem_copy : Realize ? copy R_copy.
+#intape
+cases (sem_seq … (sem_copy0 …)
+ (sem_seq … (sem_move_l …)
+ (sem_seq … (sem_adv_to_mark_l … (is_marked ?))
+ (sem_seq … (sem_clear_mark …)
+ (sem_seq … (sem_adv_to_mark_r … (is_marked ?)) (sem_clear_mark …))))) intape)
+#k * #outc * #Hloop #HR %{k} %{outc} % [@Hloop] -Hloop
+#ls #s0 #s1 #c0 #c1 #rs #l1 #l2 #l3 #Hintape #Hl1marks #Hl2marks #Hl3marks #Hlen
+#Hbits1 #Hbits2 #Hc0bits #Hc1bits
+cases HR -HR #ta * whd in ⊢ (%→?); #Hta
+cut (ta = midtape STape (〈c1,false〉::reverse ? l1@〈s1,false〉::l2@〈grid,true〉::
+ 〈merge_char c0 c1,false〉::reverse ? l1@〈s1,false〉::ls)
+ 〈comma,true〉 rs)
+[lapply (Hta ls s1 s0 rs (l1@[〈c1,false〉;〈comma,false〉]) l2 (〈grid,false〉::〈c0,false〉::l3) ?)
+ [>associative_append in ⊢ (???(????%)); normalize in ⊢ (???(??%%%)); @Hintape ]
+ -Hta #Hta cases (Hta ??? (〈s1,false〉::l1@[〈c1,false〉]) false ? ? ?? (refl ??) ?)
+ [3: #x #Hx cases (memb_append … Hx) -Hx #Hx
+ [ @Hl1marks //
+ | cases (orb_true_l … Hx) -Hx #Hx [ >(\P Hx) % | >(memb_single … Hx) % ]]
+ |4: #x #Hx cases (memb_append … Hx) -Hx #Hx
+ [ @Hl2marks //
+ | cases (orb_true_l … Hx) -Hx #Hx [ >(\P Hx) % | cases (orb_true_l … Hx) [-Hx #Hx >(\P Hx) % | @Hl3marks ] ] ]
+ |5: >length_append normalize >Hlen >commutative_plus %
+ |6: normalize >associative_append %
+ |7: #x #Hx cases (memb_append ?? (〈s1,false〉::l1) … Hx) -Hx #Hx
+ [ whd in ⊢ (??%?); >(Hbits2 … Hx) %
+ | >(memb_single … Hx) // ]
+ |8: #x #Hx cases (memb_append … Hx) -Hx #Hx
+ [ cases (orb_true_l … Hx) -Hx #Hx [ >(\P Hx) // | whd in ⊢ (??%?); >Hbits1 // @memb_append_l1 // ]
+ | >(memb_single … Hx) whd in ⊢ (??%?); >(Hbits1 〈s0,false〉) // @memb_append_l2 @memb_hd ]
+ | * #Hs1 @False_ind >Hs1 in Hbits2; #Hbits2 lapply (Hbits2 〈comma,false〉 ?) //
+ normalize #Hfalse destruct (Hfalse)
+ | * #Hs1 #Ht2 >Ht2 >reverse_cons >reverse_append >reverse_single @eq_f3 //
+ >merge_cons >merge_bits
+ [2: #x #Hx @Hbits2 cases (memb_append STape ? (reverse ? l1) ? Hx) -Hx #Hx
+ [@daemon | >(memb_single … Hx) @memb_hd ]
+ |3: >length_append >length_append >length_reverse >Hlen % ]
+ normalize >associative_append normalize >associative_append %
+ ]
+] -Hta #Hta * #tb * whd in ⊢ (%→?); #Htb
+lapply (Htb … Hta) -Htb #Htb change with (midtape ????) in Htb:(???%);
+* #tc * whd in ⊢ (%→?); #Htc
+cases (Htc … Htb)
+[ * #Hfalse normalize in Hfalse; destruct (Hfalse) ]
+* #_ #Htc
+lapply (Htc (reverse ? l1@〈s1,false〉::l2) 〈grid,true〉
+ (〈merge_char c0 c1,false〉::reverse ? l1@〈s1,false〉::ls)???)
+[ #x #Hx cases (memb_append … Hx) -Hx #Hx
+ [ @Hl1marks @daemon
+ | cases (orb_true_l … Hx) -Hx #Hx
+ [ >(\P Hx) % | @(Hl2marks … Hx) ] ]
+| %
+| whd in ⊢ (??%?); >associative_append % ] -Htc #Htc
+* #td * whd in ⊢ (%→?); #Htd lapply (Htd … Htc) -Htd #Htd
+* #te * whd in ⊢ (%→?); #Hte cases (Hte … Htd) -Hte -Htd
+[ * #Hfalse normalize in Hfalse; destruct (Hfalse) ]
+* #_ #Hte
+lapply (Hte (reverse ? (reverse ? l1@〈s1,false〉::l2)@[〈c1,false〉])
+ 〈comma,true〉 rs ? (refl ??) ?) -Hte
+[ >reverse_append >reverse_cons >reverse_reverse #x #Hx
+ cases (memb_append … Hx) -Hx #Hx
+ [ cases (memb_append … Hx) -Hx #Hx
+ [ cases (memb_append … Hx) -Hx #Hx
+ [ @daemon
+ | lapply (memb_single … Hx) -Hx #Hx >Hx % ]
+ | @(Hl1marks … Hx) ]
+ | lapply (memb_single … Hx) -Hx #Hx >Hx % ]
+| >reverse_append >reverse_reverse >reverse_cons
+ >associative_append >associative_append >associative_append
+ >associative_append >associative_append % ]
+#Hte whd in ⊢ (%→?); #Houtc lapply (Houtc … Hte) -Houtc #Houtc >Houtc
+@eq_f3 //
+>reverse_append >reverse_append >reverse_single >reverse_cons
+>reverse_append >reverse_append >reverse_reverse >reverse_reverse
+>reverse_single >associative_append >associative_append %
+qed.
\ No newline at end of file