proposition: Lemma parse'_cont : forall r s k1 k2, normal r -> (forall s', select_sub r s' s -> k1 s' = k2 s') -> parse' (r,s,k1) = parse' (r,s,k2).
proof: Proof. Proof using. intros r s. sets_eq p: (r,s). gen r s. induction_wf IH: parse_sub_wf p. introv P N E. subst p. do 2 rewrite parse'_fix. unfolds. destruct r; simpl in N. auto. apply E. hnf. rewrite~ If_r. destruct s as [|c' s']. auto. case_if~. apply E. unfolds. rewrite~ If_l. inverts N. asserts M: (forall r s', (r = r1 \/ r = r2) -> select_sub r s' s -> select_sub (regexp_alt r1 r2) s' s). introv C S. hnf in S |- *. simpl. case_if as C'. destruct C'. case_if. auto. inverts C; tryfalse. case_if~. fequals. applys~ IH. auto 7. eauto 8. applys~ IH. auto 7. eauto 8. inverts N. applys~ IH. intros s' S'. applys~ IH. intros s'' S''. apply E. hnf in S',S''|-*. simpl. tests: (productive r1); tests: (productive r2). rewrite~ If_l. applys* (@trans_inv text) s'. rewrite~ If_l. applys* trans_rclosure_l s'. rewrite~ If_l. applys* trans_rclosure_r s'. rewrite If_r; [|rew_logic;auto]. applys~ trans_rclosure s'. fequals. apply E. unfold select_sub. simpl. rewrite~ If_r. inverts N. applys~ IH. auto 7. intros s' S'. case_asserts~. applys~ IH. hnf in S'. rewrite~ If_l in S'. intros s'' S''. apply E. hnf in S'' |- *. simpls. case_if; tryfalse. inverts S''. left. applys* trans_inv. auto. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibFun LibEpsilon LibList LibInt LibNat LibProd LibSum LibRelation LibWf LibFix LibStream) ZifyNat TLC.LibNat