proposition: Lemma sublist_lookup_mask f βs l i n : sublist_lookup i n (mask f βs l) = mask f (take n (drop i βs)) <$> sublist_lookup i n l.
proof: Proof. unfold sublist_lookup; rewrite mask_length; simplify_option_eq; auto. by rewrite drop_mask, take_mask. Qed.
imports: stdpp(options)