rulesubsection23.25ex plus 1ex minus .2ex1.5ex plus .2ex

* >> ext

* >> ext

.`
H >> A|B in
by intro`

* >> A in

* >> B in

`
rulesubsection23.25ex plus
1ex minus .2ex1.5ex plus .2ex`

* >>

* >>

.`
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 >> 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

`
`

`
`

Thu Sep 14 08:45:18 EDT 1995