Next: EQUALITY Up: The Rules Previous: QUOTIENT

# SET

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

* formation . H >> ext x:A|B by intro set A new x
* >> A in
* x:A >> ext B

. 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

* canonical . 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]

Next: EQUALITY Up: The Rules Previous: QUOTIENT

Richard Eaton
Thu Sep 14 08:45:18 EDT 1995