proposition: Lemma bisimilar_mod_to_upto : forall A (E:binary A) n s1 s2, bisimilar_mod E s1 s2 -> bisimilar_mod_upto E n s1 s2.
proof: Proof. Proof using. unfold bisimilar_mod_upto. induction n; introv H. simple~. destruct s1; destruct s2; simpls. inversions H. constructor~. apply~ IHn. Qed.
imports: TLC(LibTactics LibLogic LibInt LibList LibRelation LibWf)