\forall (hds: PList).(\forall (i: nat).(\forall (t: T).(eq T (lift1 hds
(lift (S i) O t)) (lift (S (trans hds i)) O (lift1 (ptrans hds i) t)))))
\def
\forall (hds: PList).(\forall (i: nat).(\forall (t: T).(eq T (lift1 hds
(lift (S i) O t)) (lift (S (trans hds i)) O (lift1 (ptrans hds i) t)))))
\def