feat: Heterogeneous behavioural equivalences (#460)

Generalises current behavioural equivalences (bisimulation and weak
variants, simulation, and trace equivalence) to states in different
LTSs, rather than assuming that the states being compared are in the
same LTS. The convenience of homogeneous relations is retained via
abbreviations (e.g., `HomBisimilarity`) and backwards-compatible
notation.

The aim of this PR is to facilitate proving the correctness of
compilers, where states usually are in different languages.

Author: fmontesi

Cslib/Foundations/Data/Relation.lean

@@ -33,6 +33,10 @@ theorem WellFounded.iff_transGen : WellFounded (Relation.TransGen r) ↔ WellFou
 
 namespace Relation
 
+/-- The empty (heterogeneous) relation, which always returns `False`. -/
+@[nolint unusedArguments]
+def emptyHRelation {α : Sort u} {β : Sort v} (_ : α) (_ : β) := False
+
 attribute [scoped grind] ReflGen TransGen ReflTransGen EqvGen CompRel
 
 theorem ReflGen.to_eqvGen (h : ReflGen r a b) : EqvGen r a b := by