proposition: Theorem StillHappens : forall (a : B) (p : ACProcess) (ss : Discourse) (q : ACProcess) (ss1 : Discourse), Wittness a q ss1 p ss -> Always P p ss -> Always P q ss1.
proof: Proof. intros a p ss q ss1 H; elim H. intros. apply H3. apply (Always_stable P p0 ss0 c w q0). assumption. assumption. intros. apply (Always_stable P p0 ss1 cn wn q). assumption. assumption. Qed.
imports: Streams