I have type Char = cA | cB | cC | ... | cZ. If I decide to write charEq (a,b:Char ---- charEq a b:Bool) in straightforward way, I will be quickly lost in details (26^2 variants).
I tried use of refl, but cannot put it properly: let (a,b:Char; _p : Eq a b ---- charEq a b _p:Bool) and then use <= case _p does not do any good to me. I tried to figure out a type that represents equality in (eq a: EqX a a) and inequality in some other constructor, but failed. So the question is: is there any way to express equality like charEq shortly?
