proposition: Lemma mask_app f βs1 βs2 l : mask f (βs1 ++ βs2) l = mask f βs1 (take (length βs1) l) ++ mask f βs2 (drop (length βs1) l).
proof: Proof. revert l. induction βs1;intros [|??]; f_equal/=; auto using mask_nil. Qed.
imports: stdpp(options)