X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fturing%2Funiversal%2Fcopy.ma;h=b2fcf29f11e72c744719e499d0363f2b79754637;hb=637ff9311e16f1d58e03d873f84c354e1cf1e716;hp=95216acdbbd44881fa9fa009c755b1432fdd5bc1;hpb=5535cd4e08fd8d1e7e6e067eac1bb6c1bf8fcbbf;p=helm.git

diff --git a/matita/matita/lib/turing/universal/copy.ma b/matita/matita/lib/turing/universal/copy.ma
index 95216acdb..b2fcf29f1 100644
--- a/matita/matita/lib/turing/universal/copy.ma
+++ b/matita/matita/lib/turing/universal/copy.ma
@@ -292,7 +292,7 @@ lemma wsem_copy0 : WRealize ? copy0 R_copy0.
 #intape #k #outc #Hloop 
 lapply (sem_while … sem_copy_step intape k outc Hloop) [%] -Hloop
 * #ta * #Hstar @(star_ind_l ??????? Hstar)
-[ #tb whd in ⊢ (%→?); #Hleft
+[ whd in ⊢ (%→?); #Hleft
   #ls #c #c0 #rs #l1 #l3 #l4 #Htb #Hl1nomarks #Hl3l4nomarks #Hlen #l1' #bv
   #Hl1 #Hl1bits #l4' #bg #Hl4 #Hl4bits
   cases (Hleft … Htb) -Hleft #Hc #Houtc % %
@@ -302,7 +302,7 @@ lapply (sem_while … sem_copy_step intape k outc Hloop) [%] -Hloop
       #Hl1bits lapply (Hl1bits 〈c',false〉 ?) [ @memb_hd ] 
       >Hc #Hfalse destruct ]
   | @Houtc ]
-| #tb #tc #td whd in ⊢ (%→?→(?→%)→%→?); #Htc #Hstar1 #Hind #Htd
+| #tc #td whd in ⊢ (%→?→(?→%)→%→?); #Htc #Hstar1 #Hind #Htd
   lapply (Hind Htd) -Hind #Hind
   #ls #c #c0 #rs #l1 #l3 #l4 #Htb #Hl1nomarks #Hl3l4nomarks #Hlen #l1' #bv
   #Hl1 #Hl1bits #l4' #bg #Hl4 #Hl4bits %2
@@ -437,6 +437,178 @@ lapply (sem_while … sem_copy_step intape k outc Hloop) [%] -Hloop
 ]]]
 qed.
 
+definition Pre_copy0 ≝ λt1.
+  ∃ls,c,c0,rs,l1,l3,l4.
+  t1 = midtape STape (l3@l4@〈c0,true〉::ls) 〈c,true〉 (l1@rs) ∧
+  no_marks l1 ∧ no_marks (l3@l4) ∧ |l1| = |l4| ∧
+  (∃l1',bv.〈c,false〉::l1 = l1'@[〈comma,bv〉] ∧ only_bits_or_nulls l1') ∧
+  (∃l4',bg.l4@[〈c0,false〉] = 〈grid,bg〉::l4' ∧ only_bits_or_nulls l4').
+
+definition Pre_copy ≝ λt1.
+  ∃ls,s0,s1,c0,c1,rs,l1,l3,l4.
+  t1 = midtape STape (l3@〈grid,false〉::〈c0,false〉::l4@〈s0,true〉::ls) 〈s1,true〉 (l1@〈c1,false〉::〈comma,false〉::rs) ∧
+  no_marks l1 ∧ no_marks l3 ∧ no_marks l4 ∧ |l1| = |l4| ∧ 
+  only_bits (l4@[〈s0,false〉]) ∧ only_bits (〈s1,false〉::l1) ∧ 
+  bit_or_null c0 = true ∧ bit_or_null c1 = true.
+  
+lemma list_last: ∀A.∀l:list A.
+  l = [ ] ∨ ∃a,l1. l = l1@[a].
+#A #l <(reverse_reverse ? l) cases (reverse A l)
+  [%1 //
+  |#a #l1 %2 @(ex_intro ?? a) @(ex_intro ?? (reverse ? l1)) //
+  ]
+qed.
+
+lemma terminate_copy0 : ∀t.Pre_copy0 t → Terminate ? copy0 t.
+#t #HPre
+@(terminate_while_guarded ??? 
+   Pre_copy0 … 
+   (acc_Realize_to_acc_GRealize ??? Pre_copy0 … sem_copy_step)
+   … HPre) [%]
+  [ -HPre -t #t1 #t2 * #ls * #c * #c0 * #rs * #l1 * #l3 * #l4
+    * * * * * #Ht1 #Hl1nomarks #Hl3l4nomarks #Hlen
+    * #l1' * #bv * #Hl1 #Hbitsnullsl1' * #l4' * #bg * #Hl4 #Hbitsnullsl4'
+    #HR cases (HR … Ht1) -HR #Hbitnullc
+    cut (∃d1,l1''.l1 = 〈d1,false〉::l1'')
+    [ lapply Hl1nomarks cases l1 in Hl1;
+      [ whd in ⊢ (???%→?); #Hl1
+        lapply (append_l2_injective_r ? [] l1' [〈c,false〉] [〈comma,bv〉] (refl ??) Hl1)
+        #Hc destruct (Hc) normalize in Hbitnullc; destruct (Hbitnullc) 
+      | * #d #bd #l1'' #_ #Hl1nomarks >(?:bd = false) [| @(Hl1nomarks 〈d,bd〉) @memb_hd ] /3/ ] ]
+    * #d1 * #l1'' #Hl1''
+    cut (∃d2,l4''.l4 = l4''@[〈d2,false〉])
+    [ lapply Hl4 cases (list_last ? l4)
+      [ #Hl4' >Hl4' in Hlen; >Hl1'' normalize in ⊢ (%→?); #HFalse destruct (HFalse)
+      | * * #d2 #bd2 * #l4'' #Hl4'' >Hl4'' in Hl3l4nomarks; #Hl3l4nomarks #_ 
+        <(?:bd2 = false) [| @(Hl3l4nomarks 〈d2,bd2〉) @memb_append_l2 @memb_append_l2 @memb_hd ]
+        /3/ ] ]
+    * #d2 * #l4'' #Hl4'' >Hl1'' >Hl4''
+    cut (∃l1''',bv0.〈d1,false〉::l1''=l1'''@[〈comma,bv0〉]∧only_bits_or_nulls l1''')
+    [ <Hl1'' cases (list_last ? l1) in Hl1'';
+        [ #Hl1'' >Hl1''#HFalse destruct(HFalse)
+        | * #a * #l1''' #Hl1''' >Hl1''' in Hl1; #Hl1 #_
+          lapply (append_l2_injective_r ? (〈c,false〉::l1''') l1' [a] [〈comma,bv〉] (refl …) Hl1)
+          #Ha destruct (Ha) %{l1'''} %{bv} % //
+          #x #Hx @Hbitsnullsl1'
+          lapply (append_l1_injective_r ? (〈c,false〉::l1''') l1' [〈comma,bv〉] [〈comma,bv〉] (refl …) Hl1)
+          #H <H @memb_cons @Hx ] ]
+    cut (∃l4''',bg0.l4''@[〈d2,false〉]=〈grid,bg0〉::l4'''∧only_bits_or_nulls l4''')
+    [ <Hl4'' cases (list_last ? l4') in Hl4;
+        [ #Hl4' >Hl4' >Hl4'' cases l4''
+          [ normalize in ⊢ (%→?); #Hfalse destruct (Hfalse)
+          | #y #yl normalize in ⊢ (%→?); #H1 destruct (H1) cases yl in e0;
+            [ normalize in ⊢ (%→?); #Hfalse destruct (Hfalse)
+            | #z #zl normalize in ⊢ (%→?); #Hfalse destruct (Hfalse) ] ]
+        | * #a * #l4''' #Hl4''' >Hl4''' #Hl4
+          lapply (append_l1_injective_r ? l4 (〈grid,bg〉::l4''') [〈c0,false〉] [a] (refl …) Hl4)
+          -Hl4 #Hl4 >Hl4 %{l4'''} %{bg} % //
+          #x #Hx @Hbitsnullsl4' >Hl4''' @memb_append_l1 @Hx ] ]
+    #Hl4''' #Hl1'''
+    #HR cases (HR d1 (l3@l4'') c0 d2 ls (l1''@rs) ? ? ?)
+    [3: >associative_append >associative_append %
+    |4: %
+    |5: #x #Hx @Hl3l4nomarks cases (memb_append … Hx)
+      [ @memb_append_l1
+      | >Hl4'' -Hx #Hx @memb_append_l2 @memb_append_l1 @Hx ]
+    | * #x1 * #Hc #Ht2 whd >Ht2
+      %{(〈bit x1,false〉::ls)} %{d1} %{d2} %{rs} %{l1''} %{(〈bit x1,false〉::l3)} %{l4''}
+      % [ % [ % [ % [ % 
+      [ >associative_append %
+      | #x #Hx @Hl1nomarks >Hl1'' @memb_cons @Hx ]
+      | #x #Hx cases (orb_true_l … Hx) -Hx #Hx
+        [ >(\P Hx) %
+        | @Hl3l4nomarks cases (memb_append … Hx)
+          [ @memb_append_l1
+          | -Hx #Hx >Hl4'' @memb_append_l2 @memb_append_l1 @Hx ] ] ]
+      | >Hl1'' in Hlen; >Hl4'' >length_append >commutative_plus
+        normalize in ⊢ (%→?); #Hlen destruct (Hlen) @e0 ]
+      | @Hl1''' ]
+      | @Hl4''' ]
+   | * #Hc #Ht2 whd >Ht2
+      %{(〈c0,false〉::ls)} %{d1} %{d2} %{rs} %{l1''} %{(〈null,false〉::l3)} %{l4''}
+      % [ % [ % [ % [ % 
+      [ >associative_append %
+      | #x #Hx @Hl1nomarks >Hl1'' @memb_cons @Hx ]
+      | #x #Hx cases (orb_true_l … Hx) -Hx #Hx
+        [ >(\P Hx) %
+        | @Hl3l4nomarks cases (memb_append … Hx)
+          [ @memb_append_l1
+          | -Hx #Hx >Hl4'' @memb_append_l2 @memb_append_l1 @Hx ] ] ]
+      | >Hl1'' in Hlen; >Hl4'' >length_append >commutative_plus
+        normalize in ⊢ (%→?); #Hlen destruct (Hlen) @e0 ]
+      | @Hl1''' ] 
+      | @Hl4''' ]
+    ]
+ |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 % ]
+]]]
+qed.
+
 definition merge_char ≝ λc1,c2.
   match c2 with
   [ null ⇒ c1
@@ -504,23 +676,81 @@ definition R_copy ≝ λt1,t2.
                       〈merge_char c0 c1,false〉::reverse ? l1@〈s1,false〉::ls)
        〈comma,false〉 rs.
        
-axiom sem_copy0 : Realize ? copy0 R_copy0.
+lemma sem_copy0 : GRealize ? copy0 Pre_copy0 R_copy0.
+@WRealize_to_GRealize
+[ @terminate_copy0
+| @wsem_copy0 ]
+qed.
 
 definition option_cons ≝ λA.λa:option A.λl.
   match a with
   [ None ⇒ l
   | Some a' ⇒ a'::l ].
-
-
-axiom 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
+  
+lemma sem_copy : GRealize ? copy Pre_copy R_copy.
+@(GRealize_to_GRealize_2 ?? Pre_copy0 ? R_copy) //
+(* preamble: Pre_copy0 implies Pre_copy *)
+[ #t1 * #ls * #s0 * #s1 * #c0 * #c1 * #rs * #l1 * #l3 * #l4 * * * * * * * *
+  #Ht1 #Hl1nomarks #Hl3nomarks #Hl4nomarks #Hlen #Hbitsl4 #Hbitsl1 
+  #Hbitnullc0 #Hbitnullc1 whd
+  %{ls} %{s1} %{s0} %{rs} %{(l1@[〈c1,false〉;〈comma,false〉])}
+  %{l3} %{(〈grid,false〉::〈c0,false〉::l4)}
+  % [ % [ % [ % [ % 
+  [ >Ht1 -Ht1 @eq_f >associative_append %
+  | #x #Hx cases (memb_append … Hx) -Hx #Hx
+    [ @(Hl1nomarks ? Hx)
+    | cases (orb_true_l … Hx) -Hx #Hx 
+      [ >(\P Hx) %
+      | >(memb_single … Hx) % ] ] ]
+  | #x #Hx cases (memb_append … Hx) -Hx #Hx
+    [ @(Hl3nomarks ? Hx)
+    | cases (orb_true_l … Hx) -Hx #Hx
+      [ >(\P Hx) %
+      | cases (orb_true_l … Hx) -Hx #Hx
+        [ >(\P Hx) %
+        | @(Hl4nomarks ? Hx) ]]]]
+  |>length_append >Hlen >commutative_plus % ]
+  | %{(〈s1,false〉::l1@[〈c1,false〉])} %{false} %
+    [ @eq_f >associative_append %
+    | #x #Hx cases (orb_true_l … Hx) -Hx #Hx
+      [ >(\P Hx) @is_bit_to_bit_or_null @(Hbitsl1 〈s1,false〉) @memb_hd
+      | cases (memb_append … Hx) -Hx #Hx
+        [ @is_bit_to_bit_or_null @(Hbitsl1 〈\fst x,\snd x〉) @memb_cons <eq_pair_fst_snd @Hx
+        | >(memb_single… Hx) // ]
+      ]
+    ] ]
+  | %{(〈c0,false〉::l4@[〈s0,false〉])} %{false} %
+    [ %
+    | #x #Hx cases (orb_true_l … Hx) -Hx #Hx
+      [ >(\P Hx) //
+      | cases (memb_append … Hx) -Hx #Hx
+        [ @is_bit_to_bit_or_null @(Hbitsl4 〈\fst x,\snd x〉) @memb_append_l1 <eq_pair_fst_snd @Hx
+        | >(memb_single… Hx) @is_bit_to_bit_or_null @(Hbitsl4 〈s0,false〉) @memb_append_l2 @memb_hd ]
+      ]
+] ] ]
+(*whd in ⊢ (%→%)
+change with (?·?) in match copy;*)
+@(sem_seq_app_guarded ???? (λx.True) ??? sem_copy0)
+[2:@(sem_seq_app_guarded ???????? (Realize_to_GRealize … (sem_move_l (FinProd FSUnialpha FinBool))))
+  [@(λx.True)
+  |4://
+  |5:@sub_reflexive
+  |3:@(sem_seq_app_guarded ???????? (Realize_to_GRealize … (sem_adv_to_mark_l … (is_marked FSUnialpha))))
+    [@(λx.True)
+    |4://
+    |5:@sub_reflexive
+    |3:@(sem_seq_app_guarded ???????? (Realize_to_GRealize … (sem_clear_mark ?)))
+      [@(λx.True)
+      |4://
+      |5:@sub_reflexive
+      |3:@(sem_seq_app_guarded ???????? (Realize_to_GRealize … (sem_adv_to_mark_r ? (is_marked ?))))
+        [@(λx.True)
+        |4://
+        |5:@sub_reflexive
+        |3:@(Realize_to_GRealize … (sem_clear_mark ?)) ] ] ] ]
+|3: //
+|1:skip]
+#intape #outtape #HR
 #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 
@@ -553,13 +783,13 @@ cut (ta = midtape STape (〈c1,false〉::reverse ? l1@〈s1,false〉::l2@〈grid
     |3: >length_append >length_append >length_reverse >Hlen % ]
     normalize >associative_append normalize >associative_append %
   ]
-] -Hta #Hta * #tb * whd in ⊢ (%→?); #Htb
+] -Hta #Hta * #tb * * #_ #Htb
 lapply (Htb … Hta) -Htb #Htb change with (midtape ????) in Htb:(???%);
-* #tc * whd in ⊢ (%→?); #Htc 
+* #tc * * #_ #Htc 
 cases (Htc … Htb)
-[ * #Hfalse normalize in Hfalse; destruct (Hfalse) ]
-* #_ #Htc 
-lapply (Htc (reverse ? l1@〈s1,false〉::l2) 〈grid,true〉 
+(* [ * #Hfalse normalize in Hfalse; destruct (Hfalse) ] *)
+#_ #Htc cases (Htc (refl ??)) -Htc #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
@@ -567,10 +797,10 @@ lapply (Htc (reverse ? l1@〈s1,false〉::l2) 〈grid,true〉
     [ >(\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
+* #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 
+* * #_ #Hte #_ 
 lapply (Hte (reverse ? (reverse ? l1@〈s1,false〉::l2)@[〈c1,false〉])
          〈comma,true〉 rs ? (refl ??) ?) -Hte
 [ >reverse_append >reverse_cons >reverse_reverse #x #Hx
@@ -584,10 +814,9 @@ lapply (Hte (reverse ? (reverse ? l1@〈s1,false〉::l2)@[〈c1,false〉])
 | >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
+#Hte * #_ #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
+qed.
\ No newline at end of file