proposition: Lemma unfold_ACKING : forall b : bool, ACKING b = ACLISTEN Channel Act lnk1 (fun ba : bool * A => let (b1, a) := ba in if eqb b1 (negb b) then OUT (negb b) a else ACK b).
proof: Proof. intros. apply (unfold_process Channel Act (ACKING b)). Qed.
imports: ABP.ABP.BISIMULATION.Hypotheses