Data.Type.Equality
data a :=: b
sym
trans
coerce
liftEq
liftEq2
liftEq3
liftEq4
lower
class EqualityT f