X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FNaturalDeduction.v;h=cd225da363743886131b8c17b073e651c217e015;hp=2bc361f1bb0daa5c034322fa48c735d04146ae4f;hb=5a2f09b19d1cd62dee31e14625e62b32c0a02449;hpb=358d686692c40722885eaeffc7203e32142af7c8

diff --git a/src/NaturalDeduction.v b/src/NaturalDeduction.v
index 2bc361f..cd225da 100644
--- a/src/NaturalDeduction.v
+++ b/src/NaturalDeduction.v
@@ -1,5 +1,8 @@
 (*********************************************************************************************************************************)
-(* NaturalDeduction: structurally explicit proofs in Coq                                                                         *)
+(* NaturalDeduction:                                                                                                             *)
+(*                                                                                                                               *)
+(*   Structurally explicit natural deduction proofs.                                                                             *)
+(*                                                                                                                               *)
 (*********************************************************************************************************************************)
 
 Generalizable All Variables.
@@ -209,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
   }.
 
   (*