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

* >>

*

.`
H >>
x:A|B
in
by intro [new y]`

* >> A in

* y:A >> B[y/x] in

`
.
H >>
ext A|B
by intro set `

* >> ext A

* >> ext B

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

* >> A in

* >> B in

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

* >>

* >>

*

All hidden hypothesis inHbecome unhidden in the second subgoal.

.`
H >> a in x:A|B
by intro at
[new y]`

* >> a in A

* >> B[a/x]

* y:A >> B[y/x] in

`
.
H >>
A|B
ext a by intro `

* >> A ext a

* >> B ext b

All hidden hypotheses inHbecome unhidden in the second subgoal.

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

* >> a in A

* >> B ext b

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

*

*

Note that the second new hypotheses of the second subgoal is hidden.

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

* >>

*

*

`
`

Thu Sep 14 08:45:18 EDT 1995