proposition: Lemma equiv_bisimilar_mod_upto : forall A (E:binary A) n, equiv E -> equiv (bisimilar_mod_upto E n).
proof: Proof. Proof using. introv Equiv. unfold bisimilar_mod_upto. lets: (equiv_list_equiv Equiv). constructor; unfolds; dauto. Qed.
imports: TLC(LibTactics LibLogic LibInt LibList LibRelation LibWf)