proposition: Lemma R_bisim : bisimulation R.
proof: Proof. unfold R, bisimulation in |- *. repeat simple induction 1. - rewrite H1, H2; cbn; split; auto. right; split; auto. rewrite general_omega_LCons. unfold alter2, omega in |- *; trivial. rewrite general_omega_shoots_again; trivial. - rewrite H1, H2; cbn; split; auto. Qed.
imports: Arith List RelationClasses