Until Idris2 starts supporting the 'syntax' keyword, here's a poor-man's equational reasoning
data Step : a -> b -> Type
Slightly nicer syntax for justifying equations:
```
|~ a
~~ b ...( justification )
```
and we can think of the `...( justification )` as ASCII art for a thought bubble.
data FastDerivation : a -> b -> Type
(|~) : (0 x : a) -> FastDerivation x x
(~~) : FastDerivation x y -> Step y z -> FastDerivation x z
Calc : FastDerivation x y -> x = y
symHet : (0 _ : x = y) -> y = x
(..<) : (0 y : a) -> y = x -> Step x y
(..>) : (0 y : a) -> (0 _ : x = y) -> Step x y