proposition: Lemma parse_fix : forall p, parse_dom p -> parse p = Parse parse p.
proof: Proof. Proof using. applys~ (FixFun_fix_partial' (P:=parse_dom) (R:=parse_arg_sub) (F:=Parse) (f':=parse')). applys Parse_contractive_for_parse'. apply parse'_fix_Parse. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibFun LibEpsilon LibList LibInt LibNat LibProd LibSum LibRelation LibWf LibFix LibStream) ZifyNat TLC.LibNat