proposition: Lemma bisim_equi: forall n x y, bisim n x y -> x == y.
proof: Proof. cofix CIH; intros. destruct (bisim_inv _ _ _ H) as [(v & T1 & T2) | (n' & x' & y' & E1 & E2 & B')]. - apply equi_terminates with v; auto. - subst. constructor. eauto. Qed.
imports: Coq(Arith ZArith Psatz Bool String List) CDF(Sequences IMP)