Logical equivalence

Stream: computer science

[Fabrizio Montesi]

Note for logics (maybe should be an issue later on).
It would be nice to define a typeclass for relations that are 'logical equivalences'. We could call it LogicalEqv or similar. In addition to giving access to the notation \==, this class could require to prove some theorems. For example, under a given proof system (like Proof in CLL), one would expect that logical equivalence supports a substitution/congruence principle.