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

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

diff --git a/helm/EXPORT/exportprove/prove/provastruct5.v b/helm/EXPORT/exportprove/prove/provastruct5.v
new file mode 100644 (file)
index 0000000..952c9d2
--- /dev/null
+++ b/helm/EXPORT/exportprove/prove/provastruct5.v
@@ -0,0 +1,11 @@
+Section a.
+ Variable A:Prop.
+ Theorem easy:(B:Prop)B->B.
+  Exact ([H:Prop][B:Prop][b:B]b A).
+ Qed.
+ Section b.
+  Theorem easy':(B:Prop)B->B.
+   Exact easy.
+  Qed.
+ End b.
+End a.