Idris2Doc : Syntax.PreorderReasoning

Syntax.PreorderReasoning

Until Idris2 starts supporting the 'syntax' keyword, here's a
poor-man's equational reasoning
Calc : FastDerivationxy -> x = y
dataFastDerivation : a -> b -> Type
Totality: total
Constructors:
(|~) : (0 x : a) -> FastDerivationxx
(~~) : FastDerivationxy -> Stepyz -> FastDerivationxz
dataStep : 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
Constructor: 
(...) : (0 y : a) -> (0 _ : x = y) -> Stepxy