Syntax.PreorderReasoning

Until Idris2 starts supporting the 'syntax' keyword, here's a
poor-man's equational reasoning

Definitions

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.

Totality: total
Visibility: public export
Constructor: 

(...) : (0 y : a) -> (0 _ : x = y) -> Step x y

data FastDerivation : a -> b -> Type

Totality: total
Visibility: public export
Constructors:

(|~) : (0 x : a) -> FastDerivation x x

(~~) : FastDerivation x y -> Step y z -> FastDerivation x z

Calc : FastDerivation x y -> x = y

Visibility: public export

symHet : (0 _ : x = y) -> y = x

Visibility: public export

(..<) : (0 y : a) -> y = x -> Step x y

Visibility: public export
Fixity Declaration: infix operator, level 1

(..>) : (0 y : a) -> (0 _ : x = y) -> Step x y

Visibility: public export
Fixity Declaration: infix operator, level 1