update in delayed_updating

[helm.git] / matita / matita / contribs / lambdadelta / ground / etc / lib / list_rcons.etc

diff --git a/matita/matita/contribs/lambdadelta/ground/etc/lib/list_rcons.etc b/matita/matita/contribs/lambdadelta/ground/etc/lib/list_rcons.etc
new file mode 100644 (file)
index 0000000..1583e9a
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground/etc/lib/list_rcons.etc
@@ -0,0 +1,3 @@
+lemma list_rcons_prop_1 (A) (a1) (a2):
+      ⓔ ⨭ a1 ⨭{A} a2 = a1 ⨮ (ⓔ ⨭ a2).
+// qed.