proposition: Theorem parse_eq_sem_ind : forall r s k, normal r -> (parse (r,s,k) = true) = (exists s1 s2, s = s1 ++ s2 /\ sem r s1 /\ k s2 = true).
proof: Proof. Proof using. extens. iff M. apply~ parse_to_sem_ind. destruct M as (s1&s2&?&?&?). subst. apply~ sem_to_parse_ind. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibFun LibEpsilon LibList LibInt LibNat LibProd LibSum LibRelation LibWf LibFix LibStream) ZifyNat TLC.LibNat