(ptrans hds0 i) e2 e1)) (\lambda (e2: C).(getl (plus (trans hds0 i) h) c2
(CHead e2 (Bind b) (lift1 (ptrans hds0 i) v)))) x0 H7 (H9 (bge_le d (trans
hds0 i) H5))))))) H6)))) x_x)))))) H2))))))))))))))) hds).
(ptrans hds0 i) e2 e1)) (\lambda (e2: C).(getl (plus (trans hds0 i) h) c2
(CHead e2 (Bind b) (lift1 (ptrans hds0 i) v)))) x0 H7 (H9 (bge_le d (trans
hds0 i) H5))))))) H6)))) x_x)))))) H2))))))))))))))) hds).