proposition: Lemma bisimilar_mod_take : forall A (E:binary A) s1 s2, (forall i, list_equiv E (take i s1) (take i s2)) -> bisimilar_mod E s1 s2.
proof: Proof. Proof using. intros A E. cofix IH. intros. destruct s1 as [x1 s1]. destruct s2 as [x2 s2]. constructor. lets_inverts (H 1%nat). auto. apply IH. intros i. lets_inverts (H (S i)). auto. Qed.
imports: TLC(LibTactics LibLogic LibInt LibList LibRelation LibWf)