Data.Proof.EQ
data
(:=:)
liftEq
liftEq2
liftEq3
liftEq4
commEq
transEq