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

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

diff --git a/helm/EXPORT/exportprove/prove/provastruct.v b/helm/EXPORT/exportprove/prove/provastruct.v
new file mode 100644 (file)
index 0000000..503c7e0
--- /dev/null
+++ b/helm/EXPORT/exportprove/prove/provastruct.v
@@ -0,0 +1,22 @@
+Require Export Xml.
+
+Section a.
+ Variable A:Prop.
+ Section b1.
+  Variable B:Prop.
+  Axiom axiom: A -> (A -> B) ->B.
+  Theorem th1: A -> (A -> B) -> A/\B.
+   Intros A' H.
+   Split.
+   Assumption.
+   Apply axiom; Assumption.
+  Qed.
+ End b1.
+ Section b2.
+  Variable B:Set.
+  Axiom axiom': (A:Prop)A->A.
+ End b2.
+ Theorem th1': (A:Prop)A->A.
+  Auto.
+ Qed.
+End a.