proposition: Lemma REPEAT_UinvTC1 : forall (P : Prop) (w : Signal _ Act lnk1) (q : Process) (s : Stream A), UnrelProcTrans Channel Act lnk1 (REPEAT s) (Transmit _ Act lnk1 w) q -> P.
proof: Proof. intros P w q s. rewrite unfold_REPEAT. intros H1. inversion_clear H1. Qed.
imports: ABP.ABP.BISIMULATION.Hypotheses