From 5a2f09b19d1cd62dee31e14625e62b32c0a02449 Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Fri, 25 Mar 2011 11:09:55 -0700 Subject: [PATCH] add ndr_void_proofs_irrelevant --- src/NaturalDeduction.v | 3 +++ 1 file changed, 3 insertions(+) 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 }. (* -- 1.7.10.4