proposition: Lemma bisimilar_mod_upto_succ : forall A (E:binary A) n s1 s2, equiv E -> bisimilar_mod_upto E n s1 s2 -> nth n s1 = nth n s2 -> bisimilar_mod_upto E (S n) s1 s2.
proof: Proof. Proof using. introv Equiv Bis Equ. unfolds bisimilar_mod_upto. gen s1 s2. induction n; intros; destruct s1; destruct s2. simpls. subst. constructor; dauto. set_eq m: (S n). simpls. inversions Bis. constructor~. apply~ IHn. Qed.
imports: TLC(LibTactics LibLogic LibInt LibList LibRelation LibWf)