proposition: Lemma equiv_bisimilar_mod : forall A (E:binary A), equiv E -> equiv (bisimilar_mod E).
proof: Proof. Proof using. introv Equiv. constructor. unfolds. cofix IH. destruct x. constructor; dauto. unfolds. cofix IH. destruct x; destruct y; introv M. inversions M. constructor; dauto. unfolds. cofix IH. destruct x; destruct y; destruct z; introv M1 M2. inversions M1. inversions M2. constructor; dauto. Qed.
imports: TLC(LibTactics LibLogic LibInt LibList LibRelation LibWf)