proposition: Lemma parse_arg_sub_wf : wf parse_arg_sub.
proof: Proof. Proof using. intros [[r s] k]. sets_eq p: (r,s). gen k r s. induction_wf IH: parse_sub_wf p. intros. subst p. constructor. intros [[r2 s2] k2] S. applys~ IH S. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibFun LibEpsilon LibList LibInt LibNat LibProd LibSum LibRelation LibWf LibFix LibStream) ZifyNat TLC.LibNat