Many files added. Symbolic links missing. examples and contrib missing due

[helm.git] / helm / EXPORT / exportprove / prove / provastruct2.v

diff --git a/helm/EXPORT/exportprove/prove/provastruct2.v b/helm/EXPORT/exportprove/prove/provastruct2.v
new file mode 100644 (file)
index 0000000..0784e97
--- /dev/null
+++ b/helm/EXPORT/exportprove/prove/provastruct2.v
@@ -0,0 +1,42 @@
+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.