proposition: Lemma unfold_SENDING : forall (b : bool) (s : Stream A), SENDING b s = ACTALK Channel Act lnk1 (b, hd s) (SENDING b s) lnk2 (fun b1 : bool => if eqb b1 b then SEND (negb b) (tl s) else SEND b s).
proof: Proof. intros. apply (unfold_process Channel Act (SENDING b s)). Qed.
imports: ABP.ABP.BISIMULATION.Hypotheses