SET

H >> x:A|B ext a by intro at a [new y]
* >> a in A
* >> B[a/x] ext b
* y:A >> B[y/x] in

All hidden hypothesis in H become 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 in H become 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

* noncanonical . H,u: x:A|B , >> T ext ( y.t)(u) by elim u at [new y]
* y:A >> B[y/x] in
* y:A,[B[y/x] ],u=y in A >> T[y/u] ext t

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

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

* equality . H >> x:A|B = y:| in by intro [new z]
* >> A = in
* z:A >> B[z/x] -> [z/y]
* z:A >> [z/y] -> B[z/x]