Data.Type.Equality

data a :=: b

sym

trans

coerce

liftEq

liftEq2

liftEq3

liftEq4

lower

class EqualityT f