proposition: Lemma wv_u n m (e: expr3 n m): e_level e ≪ BKA -> w (v e) ≡ erase BKA e.
proof: Proof. unfold w. induction e; simpl e_level; intro Hl; try discriminate_levels; try (first [reflexivity|apply dot_weq|apply cup_weq|apply str_weq]); try (first [apply IHe1|apply IHe2|apply IHe]; solve_lower'). symmetry. simpl (erase _ _). rewrite itr_str_l, <-IHe. reflexivity. solve_lower'. simpl. now rewrite plp. Qed.
imports: Coq.PArith.BinPosDef denum lset sums normalisation kat ka_completeness untyping regex gregex lsyntax syntax lang glang boolean atoms