From: Adam Megacz <megacz@cs.berkeley.edu>
Date: Fri, 25 Mar 2011 18:09:55 +0000 (-0700)
Subject: add ndr_void_proofs_irrelevant
X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=commitdiff_plain;h=5a2f09b19d1cd62dee31e14625e62b32c0a02449;hp=94d7c55025f5df750ce213172c5d2441b5a210e1

add ndr_void_proofs_irrelevant
---

diff --git a/src/NaturalDeduction.v b/src/NaturalDeduction.v
index 407948b..cd225da 100644
--- a/src/NaturalDeduction.v
+++ b/src/NaturalDeduction.v
@@ -212,6 +212,9 @@ Section Natural_Deduction.
 
   (* 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
+
+  (* any two proofs of nothing are "equally good" *)
+  ; ndr_void_proofs_irrelevant : forall `(f:a/⋯⋯/[])(g:a/⋯⋯/[]), f === g
   }.
 
   (*