+
+-- HAll
+type family HAll f l
+type instance HAll f HNil = True
+type instance HAll f (HCons x xs) = If (Apply f x) (HAll f xs) False
+
+-- HLength
+type family HLength l
+type instance HLength HNil = D0
+type instance HLength (HCons e l) = Succ (HLength l)