proposition: Theorem Evt_stable : forall (p : ACProcess) (ss : Discourse) (c : Chnl) (w : Signal c) (q : ACProcess), Trans c p (Transmit c w) q -> ~ P p (Disc c w ss) -> Evt p (Disc c w ss) -> Evt q ss.
proof: Proof. intros. inversion H1. apply H7. change ((fun cw1 : sigS Signal => let (c, w1) return Prop := cw1 in Trans c p (Transmit c w1) q) (existS _ c w1)) in |- *. dependent rewrite H3. assumption. simpl in H0. change ((fun cw1 : sigS Signal => let (c, w1) return Prop := cw1 in ~ P p (Disc c w1 ss)) (existS _ c w1)) in |- *. dependent rewrite H3. assumption. Qed.
imports: Streams