(* we can turn an SCND without hypotheses into a ClosedND *)
Definition closedFromSCND h c (pn2:SCND h c)(cnd:ClosedND h) : ClosedND c.
refine ((fix closedFromPnodes h c (pn2:SCND h c)(cnd:ClosedND h) {struct pn2} :=
(match pn2 in SCND H C return H=h -> C=c -> _ with
| scnd_weak c => let case_weak := tt in _
| scnd_leaf ht z pn' => let case_leaf := tt in let qq := closedFromPnodes _ _ pn' in _
(* we can turn an SCND without hypotheses into a ClosedND *)
Definition closedFromSCND h c (pn2:SCND h c)(cnd:ClosedND h) : ClosedND c.
refine ((fix closedFromPnodes h c (pn2:SCND h c)(cnd:ClosedND h) {struct pn2} :=
(match pn2 in SCND H C return H=h -> C=c -> _ with
| scnd_weak c => let case_weak := tt in _
| scnd_leaf ht z pn' => let case_leaf := tt in let qq := closedFromPnodes _ _ pn' in _