rulesubsection23.25ex plus 1ex minus .2ex1.5ex plus .2ex
.
H >> 
ext A|B by intro union 
ext A 
ext B
.
H >> A|B in 
by intro
*
>> A in 
*
>> B in 
rulesubsection23.25ex plus 1ex minus .2ex1.5ex plus .2ex
.
H >> A|B ext inl(a) by intro at 
left 
.
H >> inl(a) in A|B by intro at 
*
>> a in A
*
>> B in 
.
H >> A|B ext inr(b) by intro at 
right
*
>> B ext b
*
>> A in 
.
H >> inr(b) in A|B by intro at 
*
>> b in B
*
>> A in 
rulesubsection23.25ex plus 1ex minus .2ex1.5ex plus .2ex
.
H,z:A|B,
>> T
ext decide(z;x.
;y.
)
by elim z [new x,y]
x:A,z=inl(x) in A|B >>
T[inl(x)/z]
ext 
.
H >> decide(e;x.
;y.
) in T[e/z]
*
by intro [over z.T] using A|B [new u,v]
*
>> e in A|B
*
u:A, e=inl(u) in A|B >>
[u/x]
in T[inl(u)/z]
*
v:B, e=inr(v) in A|B >>
[v/y]
in T[inr(v)/z]
rulesubsection23.25ex plus 1ex minus .2ex1.5ex plus .2ex
.
H >> decide(inl(a);x.
;y.
) = t in T by reduce 1
*
>> 
[a/x]
= t in T
.
H >> decide(inr(b);x.
;y.
) = t in T by reduce 1
*
>> 
[b/y]
= t in T