proposition: Lemma parse'_fix : forall p, parse' p = Parse' parse' p.
proof: Proof. Proof using. applys~ (FixFun_fix parse_arg_sub). intros f1 f2 [[r s] k] H. unfolds. destruct r; auto. fequal; auto 7. rewrite H; [|auto 7]. fequals_rec. apply fun_ext_1. intros s'. apply~ H. fequal. rewrite H; [|auto 7]. fequals_rec. apply fun_ext_1. intros s'. case_asserts; auto 7. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibFun LibEpsilon LibList LibInt LibNat LibProd LibSum LibRelation LibWf LibFix LibStream) ZifyNat TLC.LibNat