Data.Proof.EQ

data :=:

liftEq

liftEq2

liftEq3

liftEq4

commEq

transEq