- ⇧ 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 ($)
+ ⇧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 ($)