proposition: Lemma strong_fairness_invar : forall step e silent s, strong_fairness step silent (Cons e s) -> strong_fairness step silent s.
proof: Proof. Proof using. unfold strong_fairness. unfold inf_enabled, inf_occurred, inf_often. intros step e silent s fair l neq alev. assert (alevt_es: always (eventually (now (enabled step l))) (Cons e s)). constructor. constructor 2. destruct alev; assumption. simpl. assumption. clear alev. generalize (fair l neq alevt_es); clear fair alevt_es. intro fair; case (always_Cons fair); trivial. Qed.
imports: Verdi(Verdi) InfSeqExt(infseq exteq) Verdi(Ssrexport)