+* Where we have `H` in `X1` (the head of `ξ1`), there we could just use the bound variable `u`, right? Similarly for `G` we could just use the bound variable `v`, right? And similarly for `X2` (the head of `ξ2`). So:
+
+ ξ1 ≡ (\u v. h (X1 u v) (X2 u v)) H G
+ ξ2 ≡ (\u v. g (X1 u v) (X2 u v)) H G
+