proposition: Lemma weak_fairness_invar : forall step e silent s, weak_fairness step silent (Cons e s) -> weak_fairness step silent s.
proof: Proof. Proof using. unfold weak_fairness. unfold cont_enabled, inf_occurred, continuously, inf_often. intros step e silent s fair a neq eval. assert (eval_es: eventually (always (now (enabled step a))) (Cons e s)). apply E_next. assumption. apply fair in eval_es. apply always_invar in eval_es. assumption. assumption. Qed.
imports: Verdi(Verdi) InfSeqExt(infseq exteq) Verdi(Ssrexport)