proposition: Lemma strong_fairness_weak : forall step silent s, strong_fairness step silent s -> weak_fairness step silent s.
proof: Proof. Proof using. move => step silent. case => e s. rewrite /strong_fairness /weak_fairness /inf_enabled /cont_enabled. move => H_str l neq H_cont. apply: H_str; first by []. exact: continuously_inf_often. Qed.
imports: Verdi(Verdi) InfSeqExt(infseq exteq) Verdi(Ssrexport)