DEFINITION TList_rect()
TYPE =
ΠP:TList
→(Type:124747:cic:/matita/LAMBDA-TYPES/LambdaDelta-1/tlist/defs/TList_rect.con)
.P TNil
→(Πt:T.Πt1:TList.(P t1)→(P (TCons t t1))
→Πt:TList.(P t))
BODY =
λP:TList
→(Type:124747:cic:/matita/LAMBDA-TYPES/LambdaDelta-1/tlist/defs/TList_rect.con)
.λp:P TNil
.λf:Πt:T.Πt1:TList.(P t1)→(P (TCons t t1))
.FIXaux{
aux:Πt:TList.(P t)
:=λt:TList.<P> CASE t OF TNil⇒p | TCons t1 t2⇒f t1 t2 (aux t2)
}