proposition: Lemma SEND_SinvT : forall (P : Prop) (w : Signal _ Act del) (q : Process) (b : bool) (s : Stream A), SafeProcTrans Channel Act del (SEND b s) (Transmit _ Act del w) q -> P.
proof: Proof. intros P w q b s. rewrite unfold_SEND. intro H1. inversion H1. Defined.
imports: ABP.ABP.BISIMULATION.Hypotheses