src/HOL/ex/veriT_Preprocessing.thy

     @{term "vr1 + vr2 + vr2 :: nat"}),
    N (Trans @{term "let vr1a = vr2 in vr1 + vr1a + vr2 :: nat"},
      [N (Let [@{term "vr1 :: nat"}], [N (Refl, []), N (Refl, [])]),
       N (Let [@{term "vr2 :: nat"}], [N (Refl, []), N (Refl, [])])]));
 
-reconstruct_proof @{context} proof18
+reconstruct_proof @{context} proof25
 \<close>
 
 end