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