X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FNaturalDeduction.v;fp=src%2FNaturalDeduction.v;h=855b66a7614d31985359c0d5eb8ec09f8054aeda;hp=5cf67dba5903c933d5fa388c9fbe3eb9e176527d;hb=8cb97991a95d5761a28ca94767b8fe637d1411d9;hpb=97552c1a6dfb32098d4491951929ab1d4aca96a0

diff --git a/src/NaturalDeduction.v b/src/NaturalDeduction.v
index 5cf67db..855b66a 100644
--- a/src/NaturalDeduction.v
+++ b/src/NaturalDeduction.v
@@ -227,6 +227,9 @@ Section Natural_Deduction.
   (* products and composition must distribute over each other *)
   ; ndr_prod_preserves_comp  : forall `(f:a/⋯⋯/b)`(f':a'/⋯⋯/b')`(g:b/⋯⋯/c)`(g':b'/⋯⋯/c'), (f;;g)**(f';;g') === (f**f');;(g**g')
 
+  (* products and duplication must distribute over each other *)
+  ; ndr_prod_preserves_copy  : forall `(f:a/⋯⋯/b),                                        nd_copy a;; f**f === f ;; nd_copy b
+
   (* any two _structural_ proofs with the same hypotheses/conclusions must be considered equal *)
   ; ndr_structural_indistinguishable : forall `(f:a/⋯⋯/b)(g:a/⋯⋯/b), Structural f -> Structural g -> f===g