proposition: Lemma ACKING_UinvT : forall (P : Prop) (c : Channel) (w : Signal _ Act c) (q : Process) (b : bool), UnrelProcTrans Channel Act c (ACKING b) (Transmit _ Act c w) q -> P.
proof: Proof. intros P c w q b. rewrite unfold_ACKING. intros H1. inversion H1. Defined.
imports: ABP.ABP.BISIMULATION.Hypotheses