rulesubsection23.25ex plus 1ex minus .2ex1.5ex plus .2ex
.
H >> 
ext x:A->B by intro function A new x 
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 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:A->B ext y.b by intro at 
[new y] 
.
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
.
H,f:(x:A->B),
>> T ext t[f(a)/y]
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 when x occurs free in B, 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
.
H >> f = g in x:A->B by extensionality [new y] rulesubsection23.25ex plus 1ex minus .2ex1.5ex plus .2ex
.
H >> (
x.b)(a) = t in B by reduce 1