X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=helm%2FEXPORT%2Fexportprove%2Fprove%2Fprovastruct2.v;fp=helm%2FEXPORT%2Fexportprove%2Fprove%2Fprovastruct2.v;h=0000000000000000000000000000000000000000;hp=0784e979424e492bb6d975398b9322a0998cfd86;hb=3ef089a4c58fbe429dd539af6215991ecbe11ee2;hpb=1c7fb836e2af4f2f3d18afd0396701f2094265ff

diff --git a/helm/EXPORT/exportprove/prove/provastruct2.v b/helm/EXPORT/exportprove/prove/provastruct2.v
deleted file mode 100644
index 0784e9794..000000000
--- a/helm/EXPORT/exportprove/prove/provastruct2.v
+++ /dev/null
@@ -1,42 +0,0 @@
-Section init.
-Section a.
- Section a1.
-  Section a11.
-   Section a111.
-    Local uno := (S O).
-   End a111.
-   Section a112.
-   End a112.
-   Section a113.
-   End a113.
-  End a11.
-  Local uno := (S O).
- End a1.
- Section a2.
-  Section a21.
-   Local uno := (S O).
-  End a21.
-  Section a22.
-   Section a221.
-   End a221.
-  End a22.
-  Section a23.
-   Section a231.
-    Section a2311.
-     Local uno := (S O).
-    End a2311.
-    Section a2312.
-    End a2312.
-    Section a2313.
-    End a2313.
-   End a231.
-   Section a232.
-    Section a2321.
-    End a2321.
-   End a232.
-  End a23.
-  Local uno := (S O).
- End a2.
- Definition uno := (S O).
-End a.
-End init.