- ⇧ T m$ xs m$ ⇧ f
-== ⇧ T m$ ((⇧ id) m$ xs) m$ ⇧ f, by 1
-== ⇧ (○) m$ ⇧ T m$ ⇧ id m$ xs m$ ⇧ f, by 3
-== ⇧ ($id) m$ (⇧ (○) m$ ⇧ T) m$ xs m$ ⇧ f, by 4
-== ⇧ (○) m$ ⇧ ($id) m$ ⇧ (○) m$ ⇧ T m$ xs m$ ⇧ f, by 3
-== ⇧ ((○) ($id)) m$ ⇧ (○) m$ ⇧ T m$ xs m$ ⇧ f, by 2
-== ⇧ ((○) ($id) (○)) m$ ⇧ T m$ xs m$ ⇧ f, by 2
-== ⇧ id m$ ⇧ T m$ xs m$ ⇧ f, by definitions of ○ and $
-== ⇧ T m$ xs m$ ⇧ f, by 1
-== ⇧ ($f) m$ (⇧ T m$ xs), by 4
-== ⇧ (○) m$ ⇧ ($f) m$ ⇧ T m$ xs, by 3
-== ⇧ ((○) ($f)) m$ ⇧ T m$ xs, by 2
-== ⇧ ((○) ($f) T) m$ xs, by 2
-== ⇧ f m$ xs, by definitions of ○ and $ and T == flip ($)
+ ⇧ T ¢ xs ¢ ⇧ f
+== ⇧ T ¢ ((⇧ id) ¢ xs) ¢ ⇧ f, by 1
+== ⇧ (○) ¢ ⇧ T ¢ ⇧ id ¢ xs ¢ ⇧ f, by 3
+== ⇧ ($id) ¢ (⇧ (○) ¢ ⇧ T) ¢ xs ¢ ⇧ f, by 4
+== ⇧ (○) ¢ ⇧ ($id) ¢ ⇧ (○) ¢ ⇧ T ¢ xs ¢ ⇧ f, by 3
+== ⇧ ((○) ($id)) ¢ ⇧ (○) ¢ ⇧ T ¢ xs ¢ ⇧ f, by 2
+== ⇧ ((○) ($id) (○)) ¢ ⇧ T ¢ xs ¢ ⇧ f, by 2
+== ⇧ id ¢ ⇧ T ¢ xs ¢ ⇧ f, by definitions of ○ and $
+== ⇧ T ¢ xs ¢ ⇧ f, by 1
+== ⇧ ($f) ¢ (⇧ T ¢ xs), by 4
+== ⇧ (○) ¢ ⇧ ($f) ¢ ⇧ T ¢ xs, by 3
+== ⇧ ((○) ($f)) ¢ ⇧ T ¢ xs, by 2
+== ⇧ ((○) ($f) T) ¢ xs, by 2
+== ⇧ f ¢ xs, by definitions of ○ and $ and T == flip ($)