fact: CoInductive Always : ACProcess -> Discourse -> Prop := always : forall (c : Chnl) (w : Signal c) (s : Discourse) (p : ACProcess), P p (Disc c w s) -> (forall q : ACProcess, Trans c p (Transmit c w) q -> Always q s) -> Always p (Disc c w s).
imports: Streams