proposition: Lemma parse'_fix_Parse : fixed_point (pfun_equal parse_dom) Parse parse'.
proof: Proof. Proof using. intros f Hf [[r s] k] N. asserts E: (pfun_equal parse_dom f parse'). unfolds. apply~ equiv_sym. clear Hf. rewrite~ E. rewrite parse'_fix. unfold Parse, Parse'. destruct r; auto; simpl in N. inverts N. fequals; rewrite~ E. inverts N. rewrite~ E. apply~ parse'_cont. intros s' S'. rewrite~ E. inverts N. fequals. rewrite~ E. apply~ parse'_cont. intros s' S'. hnf in S'. rewrite~ If_l in S'. case_asserts; auto_false. rewrite~ E. simple~. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibFun LibEpsilon LibList LibInt LibNat LibProd LibSum LibRelation LibWf LibFix LibStream) ZifyNat TLC.LibNat