proposition: Lemma ACK_UinvTC1 : forall (P : Prop) (v : bool * A) (q : Process) (b : bool), UnrelProcTrans Channel Act lnk1 (ACK b) (Transmit _ Act lnk1 (Clear _ Act lnk1 v)) q -> P.
proof: Proof. intros P w q b. rewrite unfold_ACK. intro H1. inversion H1. Defined.
imports: ABP.ABP.BISIMULATION.Hypotheses