+definition rpseq: Type[0] \def list rptr.
+
+(* Note: a "spine" computation contracts just redexes in the spine *)
+definition is_spine: predicate rpseq ≝ λs.
+ All … in_spine s.
+
+(* Note: to us, a "normal" computation contracts redexes in non-decreasing positions *)
+definition is_le: predicate rpseq ≝ λs.
+ Allr … rple s.