proposition: Lemma unfold_SEND : forall (b : bool) (s : Stream A), SEND b s = ACTALK Channel Act lnk1 (b, hd s) (SENDING b s) lnk2 (fun _ : bool => SEND b s).
proof: Proof. intros. apply (unfold_process Channel Act (SEND b s)). Qed.
imports: ABP.ABP.BISIMULATION.Hypotheses