proposition: Lemma strong_fairness_extensional : forall step silent, extensional (strong_fairness step silent).
proof: Proof. Proof using. move => step silent. rewrite /extensional /strong_fairness /inf_enabled /inf_occurred /=. move => s1 s2 H_eq H_s1 l' H_neq' H_en. have H_s1l := H_s1 l'. move: H_s1l. set s1i := inf_often (now (occurred _)) s1. move => H_s1l. suff H_suff: s1i. move: H_suff. apply extensional_inf_often => //. exact: extensional_now. apply: H_s1l => {s1i}; first by []. move: H_en. apply: extensional_inf_often; last exact: exteq_sym. exact: extensional_now. Qed.
imports: Verdi(Verdi) InfSeqExt(infseq exteq) Verdi(Ssrexport)