--- a/src/HOL/ex/veriT_Preprocessing.thy Wed Oct 31 15:53:32 2018 +0100
+++ b/src/HOL/ex/veriT_Preprocessing.thy Thu Nov 01 09:25:58 2018 +0100
@@ -467,4 +467,15 @@
reconstruct_proof @{context} proof24
\<close>
+ML \<open>
+val proof25 =
+ ((@{term "let vr0 = vr1 in let vr1 = vr2 in vr0 + vr1 + vr2 :: nat"},
+ @{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
+\<close>
+
end