proposition: Lemma frel_comp {A B C: Set} (f: A -> B) (g: B -> C): frel f ⋅ frel g ≡ frel (fun x => g (f x)).
proof: Proof. apply antisym. intros x z [y -> ->]. reflexivity. simpl. intros x z ->. eexists; reflexivity. Qed.
imports: boolean prop kat