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

* >> ext A

* >> ext B

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

* >> A in

* >> B in

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

*

* >>

.`
H >>
x.b in y:A->B by intro at
[new z] `

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

* >> A in

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

by elim **f** on **a** [new **y**]
>> **a** in **A**

*
**y**:**B**[**a**/**x**]
,
**y**=**f**(**a**) in **B**[**a**/**x**]
>> **T** ext **t**

.`
H,f:(x:A->B), >> T ext t[f(a)/y]
`

`
by elim f [new y] `

* >> A ext a

* y:B >> T ext t

The first form is used whenxoccurs free inB, the second when it doesn't.

.`
H >> f(a) in B[a/x]
by intro using x:A->B `

* >> f in x:A->B

* >> a in A

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

*

* >>

* >>

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

* >>

`
`

Thu Sep 14 08:45:18 EDT 1995