rulesubsection23.25ex plus 1ex minus .2ex1.5ex plus .2ex
.
H >> 
ext void by intro void
.
H >> void in 
by intro
rulesubsection23.25ex plus 1ex minus .2ex1.5ex plus .2ex
.
H,z:void >> T ext any(z) by elim z
.
H >> any(e) in T by intro
*
>> e in void