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

* >> ext

.`
H >> A list in
by intro `

* >> A in

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

* >>

.`
H >> nil in A list by intro at
`

* >> A in

`
.
H >> A list ext h.t by intro . `

* >> A ext h

* >> A list ext t

`
.
H >> in A list by intro `

* >> a in A

* >> b in A list

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

* by elim

* >>

*

>> **T**[/**x**]
ext

.`
H >> list_ind(e;;) in T[e/z]
`

* by intro [over ] using A list [new u,v,w]

* >> e in A list

* >> in T[nil/z]

* u:A,v:A list,w:T[v/z]

* >> [u,v,w/x,y,z] in T[u.v/z]

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

.`
H >> list_ind(nil;;) = t in T by reduce 1 `

* >> = t in T

`
.
H >> list_ind(;;) = t in T by reduce 1 `

* >> [a,b,list_ind(b;;)/u,v,w]

`
= t in T
`

`
`

`
`

Thu Sep 14 08:45:18 EDT 1995