Documentation

Elaboration functionf for binrel% and binrel_no_prop% notations. We use the infrastructure for binop% to make sure we propagate information between the left and right hand sides of a binary relation.

Recall that the binrel_no_prop% notation is used for relations such as == which do not support Prop, but we still want to be able to write (5 > 2) == (2 > 1).

If noProp == true and e has type Prop, then coerce it to Bool.

Step-wise reasoning over transitive relations.

calc
  a = b := pab
  b = c := pbc
  ...
  y = z := pyz

proves a = z from the given step-wise proofs. = can be replaced with any relation implementing the typeclass Trans. Instead of repeating the right- hand sides, subsequent left-hand sides can be replaced with _.