Data.Type.Equality

data a :=: b

sym

trans

subst

subst2

cong

cong2

cong3

coerce

class EqT f

class EqT2 f

class EqT3 f