-definition lifts1:
- PList \to (TList \to TList)
-\def
- let rec lifts1 (hds: PList) (ts: TList) on ts: TList \def (match ts with
-[TNil \Rightarrow TNil | (TCons t ts0) \Rightarrow (TCons (lift1 hds t)
-(lifts1 hds ts0))]) in lifts1.
+rec definition lifts1 (hds: PList) (ts: TList) on ts: TList \def match ts
+with [TNil \Rightarrow TNil | (TCons t ts0) \Rightarrow (TCons (lift1 hds t)
+(lifts1 hds ts0))].