proposition: Lemma mask_mask f g βs1 βs2 l : (∀ x, f (g x) = f x) → βs1 =.>* βs2 → mask f βs2 (mask g βs1 l) = mask f βs2 l.
proof: Proof. intros ? Hβs. revert l. by induction Hβs as [|[] []]; intros [|??]; f_equal/=. Qed.
imports: stdpp(options)