a contribution about subset theory in an intuitionistic and predicative foundation

[helm.git] / helm / coq-contribs / SUBSETS / Toolbox.v

diff --git a/helm/coq-contribs/SUBSETS/Toolbox.v b/helm/coq-contribs/SUBSETS/Toolbox.v
new file mode 100644 (file)
index 0000000..9217ef9
--- /dev/null
+++ b/helm/coq-contribs/SUBSETS/Toolbox.v
@@ -0,0 +1,12 @@
+Require Export st_base.
+Require Export st_logic.
+Require Export st_nat.
+Require Export st_arith.
+Require Export Standard.
+Require Export xt_fin.
+Require Export tbs_base.
+Require Export tbs_rel.
+Require Export tbs_op.
+Require Export tbs_rop.
+Require Export tbs_fun.
+Require Export tbs_fin.