rulesubsection23.25ex plus 1ex minus .2ex1.5ex plus .2ex
.
H >> 
ext A list by intro list 
ext A
.
H >> A list in 
by intro
*
>> A in 
rulesubsection23.25ex plus 1ex minus .2ex1.5ex plus .2ex
.
H >> A list ext nil by intro nil at 
.
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
.
H,x:A list,
>> T
ext list_ind(x;
;u,v,w.
) 
>> 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