proposition: Lemma SEND_ULoosed : forall (b : bool) (s : Stream A) (p3 : Process), UnrelProcTrans Channel Act lnk1 (SEND b s) (Transmit Channel Act lnk1 (Noise Channel Act lnk1)) p3 -> p3 = SENDING b s.
proof: Proof. intros b s p3. pattern (SEND b s) at 1 in |- *; rewrite unfold_SEND. intro H. inversion H. trivial. Defined.
imports: ABP.ABP.BISIMULATION.Hypotheses