[PVS-Help] I want to ask you some questions

hello, Please forgive me that I don't know how to call you.I am a PVS user of China,and in my study of PVS ,I come across some problems.Two of these is following:
1.  I want to use pvs to express the axiomatization of Propositional Projection Temporal Logic(PPTL),but I don't know how to express "prj",that is (P1,P2,P3,....Pm) prj Q ,where Pi(1<=i<=m) and Q is a formula in PPTL.I'd like to use " list",is it suitable?
2. in following specification ,there is a mistake in if _expression_ ,but I can't understand why and how to correct ,so can you help me if you have time ? Thank you very much.

a part of the specification is :

sequ[ T : TYPE ] : THEORY

BEGIN

sequ : TYPE = [# infinite : bool, len : nat, seq : ARRAY[{ i:nat | infinite or i<=len } -> T ] #]

END sequ

ftp : var sequ[form] %form is formulas

prjns(ftp)(i:nat,l:nat,n:{j:nat|j>=1}) : sequ[form] =

let m=(n-1)*(l-i+1) in (#infinte := infinite(ftp),len := len(ftp)+m,seq :=

( LAMBDA (k: nat):

(if ( k <= l )  then seq(ftp)(k)

elsif (k< m+l) then

(LAMBDA (t:{j:nat|1<=j<=l-i+1}): seq(ftp)(i+t-1))

else (LAMBDA (x:{j:nat|l<j<=len(ftp)}): seq(ftp)(x))   endif))#)

this is the mistake:
Expecting an _expression_
No resolution for IF with arguments of possible types:
(k <= l) : booleans.bool
IF (k < m + l)
THEN (LAMBDA (t: {j: nat | b2n(1 <= j) <= l - i + 1}): seq(ftp)(i + t - 1))
ELSE (LAMBDA (x: {j: nat | b2n(l < j) <= len(ftp)}): seq(ftp)(x)) : [{j:
naturalnumbers.nat |
reals.<=
(bit.b2n
(reals.<=                                                                                     (1,j)),
(number_fields.-)
((number_fields.+)
l),
i))} ->

P.S : thank you a lot,