[be5invis]

You say you have dependent types

OK, could you define this?

    data Eq : {a : Type} -> a -> a -> Type where
        Refl : Eq x x

    sym : {x : a} -> {y : a} -> Eq x y -> Eq y x
    sym Refl = Refl

    replace : {a : Type} -> {x : a} -> {y : a} -> {f : a -> Type} -> Eq x y -> f x -> f y
    replace Refl p = p