proposition: Lemma sem_to_parse_ind : forall r s s' k, sem r s -> normal r -> k s' = true -> parse (r, s ++ s', k) = true.
proof: Proof. Proof using. introv S N K. gen s' k N. induction S; intros; (rewrite parse_fix; [ | apply N ]); unfold Parse at 1; simpl in N; (try match type of N with _ /\ _ => destruct N end). rew_list~. rew_list. rewrite~ If_l. rewrite~ IHS. rewrite IHS at 1; auto. rew_bool~. rew_list. auto. rew_list. rewrite~ K. rew_list. rewrite~ IHS1. rew_bool~. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibFun LibEpsilon LibList LibInt LibNat LibProd LibSum LibRelation LibWf LibFix LibStream) ZifyNat TLC.LibNat