From: Adam Megacz <megacz@cs.berkeley.edu>
Date: Sat, 19 Mar 2011 21:15:14 +0000 (-0700)
Subject: add closedNDtoNormalND to NaturalDeduction
X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=commitdiff_plain;h=358d686692c40722885eaeffc7203e32142af7c8

add closedNDtoNormalND to NaturalDeduction
---

diff --git a/src/NaturalDeduction.v b/src/NaturalDeduction.v
index f8baff0..2bc361f 100644
--- a/src/NaturalDeduction.v
+++ b/src/NaturalDeduction.v
@@ -299,6 +299,14 @@ Section Natural_Deduction.
     apply q2. subst. apply cnd0.
     Defined.
 
+  (* undo the above *)
+  Fixpoint closedNDtoNormalND {c}(cnd:ClosedND c) : ND [] c :=
+  match cnd in ClosedND C return ND [] C with
+  | cnd_weak                   => nd_id0
+  | cnd_rule   h c cndh rhc    => closedNDtoNormalND cndh ;; nd_rule rhc
+  | cnd_branch c1 c2 cnd1 cnd2 => nd_llecnac ;; nd_prod (closedNDtoNormalND cnd1) (closedNDtoNormalND cnd2)
+  end.
+
   Close Scope nd_scope.
   Open Scope pf_scope.