proposition: Lemma Parse_contractive_for_parse' : forall f' p, parse_dom p -> (forall q, parse_dom q -> parse_arg_sub q p -> parse' q = f' q) -> Parse parse' p = Parse f' p.
proof: Proof. Proof using. introv N IH. unfold Parse. destruct p as [[r s] k]. hnf in N. destruct r; simpl in N; auto. inverts N. fequals; apply~ IH. inverts N. erewrite parse'_cont; auto. apply~ IH. simpl. intros s' S'. apply~ IH. inverts N. fequals. erewrite parse'_cont; auto. apply IH; auto 7. simpl. intros s' S'. hnf in S'. rewrite~ If_l in S'. apply~ IH; hnfs~. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibFun LibEpsilon LibList LibInt LibNat LibProd LibSum LibRelation LibWf LibFix LibStream) ZifyNat TLC.LibNat