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