proposition: Lemma SENDING_UinvT2 : forall (P : Prop) (w : Signal _ Act lnk2) (q : Process) (b : bool) (s : Stream A), UnrelProcTrans Channel Act lnk2 (SENDING b s) (Transmit _ Act lnk2 w) q -> P.
proof: Proof. intros P w q b s. rewrite unfold_SENDING. intros H2. inversion H2. Defined.
imports: ABP.ABP.BISIMULATION.Hypotheses