proposition: Corollary parse_to_sem : forall r s, normal r -> parse (r,s,is_nil) = true -> sem r s.
proof: Proof. Proof using. intros. forwards~ (s1&s2&E&S&K): (@parse_to_sem_ind r s is_nil). subst. destruct s2; tryfalse. rew_list~ in *. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibFun LibEpsilon LibList LibInt LibNat LibProd LibSum LibRelation LibWf LibFix LibStream) ZifyNat TLC.LibNat