proposition: Lemma unfold_REPEAT : forall s : Stream A, REPEAT s = ACTALK Channel Act del (hd s) (REPEAT (tl s)) del (fun _ : A => REPEAT s).
proof: Proof. intros. apply (unfold_process Channel Act (REPEAT s)). Qed.
imports: ABP.ABP.BISIMULATION.Hypotheses