proposition: Lemma clean_str' n (e: guards n n): clean e -> clean (g_str' e).
proof: Proof. induction e; intro Hae; simpl g_str'. apply clean_one'. assert (He: clean e) by (intros ? ?; apply Hae; now right). specialize (IHe He). assert (Ha: clean1 a) by (apply Hae; now left). clear Hae. apply clean_cup. assumption. apply clean_dot'. assumption. apply clean_dot'. apply clean_cup. 2: apply clean_one'. 2: apply clean_dot'; [now apply clean_single | assumption]. revert IHe. generalize (g_str' e). clear e He. intros e He. apply clean_single. unfold clean1. unfold geval. simpl o; simpl v; fold_regex. rewrite 2dotA, <-str_itr, <-2itr_str_l. rewrite G.lang_dot, G.lang_itr, G.lang_dot, G.lang_sup, G.lang_atom. rewrite R.lang_dot, R.lang_itr, R.lang_dot, o_sup, v_sup, R.lang_sup. repeat change (o_pred ?a (atom ?b)) with (o (g_atom a b)). setoid_rewrite R_lang_atom. apply gl_itr. rewrite 2dotxsum, 2dotsumx, gl_sup. apply sup_weq'. reflexivity. intros f Hf. apply clean_inner_dot. apply Ha. apply He, Hf. Qed.
imports: Coq.PArith.BinPosDef denum lset sums normalisation kat ka_completeness untyping regex gregex lsyntax syntax lang glang boolean atoms