proposition: Lemma to_gregex_eval {L: laws X} v n m e fp: e_level e ≪ BKA -> vars e ≦ v -> eval fp n m e ≡ gregex.eval f' (fun n i => fp n (nth i v xH)) (fun i => val (fs i)) (to_gregex v n m e).
proof: Proof. induction e; simpl e_level; simpl (vars _); intros Hl Hv; try discriminate_levels; simpl; rewrite ?union_app in Hv. reflexivity. symmetry. apply kat.inj_top. apply cup_weq. apply IHe1. solve_lower'. rewrite <- Hv. lattice. apply IHe2. solve_lower'. rewrite <- Hv. lattice. apply dot_weq. apply IHe1. solve_lower'. rewrite <- Hv. lattice. apply IHe2. solve_lower'. rewrite <- Hv. lattice. apply itr_weq, IHe. solve_lower'. assumption. rewrite kat.inj_top, <-str_itr. apply str_weq, IHe. solve_lower'. assumption. destruct a as [a|[n p]]. reflexivity. simpl. apply kat.inj_weq. clear Hl. induction p; simpl; simpl (lsyntax.vars _) in Hv; rewrite ?union_app in Hv. reflexivity. reflexivity. apply cup_weq. apply IHp1. rewrite <-Hv. lattice. apply IHp2. rewrite <-Hv. lattice. apply cap_weq. apply IHp1. rewrite <-Hv. lattice. apply IHp2. rewrite <-Hv. lattice. apply neg_weq, IHp. assumption. simpl. destruct (in_idx a v) as [j [-> Hj]]. apply Hv; now left. simpl. now rewrite Hj. Qed.
imports: lsyntax ordinal lset positives kat gregex syntax