commit by user mkmluser

[helm.git] / weblib / cicm2012 / disambiguation.ma

diff --git a/weblib/cicm2012/disambiguation.ma b/weblib/cicm2012/disambiguation.ma
new file mode 100644 (file)
index 0000000..f1665c1
--- /dev/null
+++ b/weblib/cicm2012/disambiguation.ma
@@ -0,0 +1,5 @@
+include "cicm2012/naturals.ma".
+include "cicm2012/rationals.ma".
+include "cicm2012/reals.ma".
+
+lemma associative_plus : ∀x,y,z.add (add x y) z = add x (add y z).
\ No newline at end of file