proposition: Lemma unfold_OUT : forall (b : bool) (a : A), OUT b a = ACTALK Channel Act del a (ACK b) lnk1 (fun _ : bool * A => OUT b a).
proof: Proof. intros. apply (unfold_process Channel Act (OUT b a)). Qed.
imports: ABP.ABP.BISIMULATION.Hypotheses