proposition: Lemma fhrel_weq_dec A B (e1 e2 : {fhrel A & B}) : decidable (e1 ≡ e2).
proof: Proof. apply: (@decP _ [forall x, forall y, e1 x y == e2 x y]). apply: (equivP idP); to_prop; reflexivity. Qed.
imports: Setoid Morphisms kat normalisation rewriting kat_tac comparisons rel relalg boolean mathcomp(all_ssreflect)