Used simplifier rules/spec theorems by specification

Used from specification nat

• nat/add-01 is used by infapp-one-to-succ2, cons-eq-inf, from-cons-one, appinf-one-to-succ, appinf-one-get-succ, get-cons-succ, one-inf, to-succ-cons, tl-lem, appinf-one-to-succ2, appinf-one-get-succ2, cons-eq, tl-inf-1, infapp-one-to-succ,
• nat/anti is used by appinf-to-ge, append-from-ge-01,
• nat/cancel-01 is used by from-append-add, append-to-gr-01, infapp-from-le, infapp-assoc,
• nat/elim-pred-c is used by cons-to-addnum, cons-from-addnum, cons-eq-inf, expand-cons, intrace-expand, get-cons-num, elim-hd-tl, cons-to-num, append-to-gr-01, get-infto, from-succ, contractinf-tl, contractinf-from1, cons-from-num, to-unwind-end,
• nat/elim-sub is used by append-from-gt, infapp-get-ge, infapp-to-ge, to-plus-from-inf-simp, append-from-gr-01, appinf-to-split, from-append-tofrom, infapp-from-gt, append-assoc, swap-inf-to-from, append-to-gr-01, swap-inf-to-from-app, swap-to-from, infapp-assoc, get-append-notls, swap-to-from-app,
• nat/eq-01 is used by from-append-add, infapp-from-gt, append-from-addsize, append-assoc, append-to-addsize-01, appinf-get-ge-01, infapp-inj, appinf-to-ge-01, append-to-gr-01, swap-inf-to-from-app, infapp-get-eqadd, get-append-notls, swap-to-from-app, to-append-add,
• nat/eqle-one is used by to-to-leq-inf,
• nat/fle is used by appinf-to-split, fin-to-to-ls,
• nat/fle-01 is used by infapp-to-le, from-append-tofrom, append-assoc, infapp-assoc,
• nat/l-num-05 is used by to-inf-two,
• nat/l-num-06 is used by append-to-gr-01, appinf-one-get-succ2,
• nat/le-add is used by append-to-addsize-01, appinf-to-ge-01, swap-to-from-app, to-append-add,
• nat/le-def is used by infapp-to-ge-01, appinf-to-split, from-append-tofrom, from-append-add, size-from-less, append-assoc, append-to-size-01, to-to-leq-inf, appinf-to-ge-01, length-from, infapp-assoc, less-size-from, swap-to-from-app,
• nat/le-ls-simp is used by appinf-get-ge, fin-to-to-leq, fin-to-to-eq, appinf-to-split, from-append-tofrom, from-append-add, ton-fromn-fin, get-from, fin-to-to-ls,
• nat/le-num-06 is used by appinf-one-to-succ2,
• nat/lels is used by get-to, append-le-to, to-plus-from-inf-simp, to-from-01, append-from-ge-02, append-from-ge-01, fin-to-to-leq, infapp-to-ge-01, fin-to-to-eq, infapp-to-le, get-toinf, appinf-to-split, from-append-tofrom, from-append-add, to-plus-from-fin-simp, size-from-less, append-assoc, size-from, append-to-addsize-01, to-to-leq, ton-fromn-fin, get-from, get-finto, to-empty2, size-to, fin-to-to-ls, fin-size-from, get-infto, elim-fromto, from-succ, toinf-to-leq, to-inf-two, infapp-assoc, get-append-notls, to-unwind-end-fin, ton-fromn, swap-to-from-app, to-append-add,
• nat/lels-03 is used by append-from-gt, to-to-ls, append-from-gr-01, appinf-to-split, infapp-from-gt, append-to-gr-01,
• nat/lep is used by infapp-to-le, from-append-tofrom, swap-inf-to-from, infapp-from-le, swap-inf-to-from-app, swap-to-from, infapp-assoc, get-append-notls, swap-to-from-app,
• nat/lep-02 is used by to-to-leq-inf, append-to-le-01, append-from-le-01, infapp-assoc,
• nat/ler is used by append-from-ge-02, to-to-eq-inf, to-to-eq,
• nat/les is used by to-to-leq-inf,
• nat/let is used by fin-to-to-leq,
• nat/lez-01 is used by to-to-leq-inf, append-to-le-01, append-from-le-01,
• nat/ls is used by from-append-add, less-size-from,
• nat/ls-01 is used by infapp-to-ge-01, appinf-to-split, from-append-tofrom, size-from-less, append-assoc,
• nat/ls-le-simp is used by get-to, to-plus-from-inf-simp, infapp-to-ge-01, infapp-to-le, get-toinf, appinf-to-split, from-append-tofrom, from-append-add, size-from-less, size-from, size-to, fin-size-from, to-inf-two, infapp-assoc, ton-fromn,
• nat/pred-03 is used by expand-cons, intrace-expand, elim-hd-tl, from-cons-one, get-cons-zero, cons-append, get-cons-succ, one-inf, to-succ-cons, from-succ, tl-inf-1, to-unwind-end,
• nat/prop-07 is used by appinf-to-split,
• nat/sub-base is used by empty-append, infapp-empty, append-to-gr-01,
• nat/succ-01 is used by to-from-01, appinf-one-to-succ, get-infto, from-succ, to-unwind-end-fin,
• nat/zero is used by append-from-ge-02, append-from-ge-01, infapp-get-eq, ton-fromn-fin, ton-fromn-inf, swap-to-from-app,
• nat/zero-02 is used by appinf-to-ge,

Used from specification stream

• stream/append-from-le is used by append-from-le,
• stream/append-from-size is used by append-from-size,
• stream/fin-finlen-tolen is used by to-all,
• stream/from-cons-one-fin is used by from-cons-one-fin,
• stream/from-succ-cons-l-lem is used by from-succ-cons-l-lem, to-from-01, from-all, from-to-exchange, from-succ, append-from-le-01,
• stream/single-to-one is used by to-to-leq-inf, single-to-one,
• stream/to-plus-from-fin is used by to-plus-from-fin, elim-fromto,
• stream/to-succ-cons-l-lem is used by to-from-01, to-all, to-succ-cons-l-lem, append-to-le-01, to-unwind-end-fin,

Used from specification nat-inf

• nat-inf/notinf-fin is used by leq-prefix,
• nat-inf/num-add is used by toinf-add,
• nat-inf/add-all-inf is used by size-append, toinftoinf-append-add,
• nat-inf/add-all-zero is used by get-from-zero, from-to-exchange,
• nat-inf/add-assoc is used by size-append, prefix-notsmallersize, extensionality-to, leq-prefix, from-infto-exchange, get-from-zero, toinf-empty3, from-append-tofrom, from-append-add, size-from-less, to-is-prefix, toinfto-append-add, get-from, to-empty3, nlslen-lslensn-eqlensn, append-notsmallersize1, append-notsmallersize2, from-to-exchange, contractinf-tl, size-succ, contractinf-from1, less-size-from, to-unwind-end, swap-to-from-app, toinftoinf-append-add, from-append-toinffrom, to-append-add,
• nat-inf/add-cancel-num-02 is used by from-to-exchange,
• nat-inf/add-comm is used by size-append, prefix-notsmallersize, extensionality-to, leq-prefix, from-infto-exchange, get-from-zero, toinf-empty3, from-append-tofrom, from-append-add, size-from-less, to-is-prefix, toinfto-append-add, get-from, to-empty3, nlslen-lslensn-eqlensn, append-notsmallersize1, append-notsmallersize2, from-to-exchange, contractinf-tl, swap-to-from, size-succ, contractinf-from1, less-size-from, to-unwind-end, swap-to-from-app, toinftoinf-append-add, from-append-toinffrom, to-append-add,
• nat-inf/add-fin is used by from-from, size-append, extensionality-to, to-unwind-end2, from-append-tofrom, from-append-add, size-from-less, to-empty3, from-to-exchange, swap-inf-to-from-app, swap-to-from, less-size-from, to-unwind-end, swap-to-from-app, from-append-toinffrom, to-append-add,
• nat-inf/add-inf1 is used by contractinf-tl,
• nat-inf/add-inf2 is used by size-append, from-infto-exchange, toinf-empty3, from-append-add, toinfto-append-add, contractinf-from1, from-append-toinffrom,
• nat-inf/add-less-fin-01 is used by leq-prefix, to-is-prefix,
• nat-inf/add-ls-cancel-01 is used by from-append-add,
• nat-inf/add-ls-cancel-num-04 is used by from-to-exchange,
• nat-inf/add-not-less is used by prefix-notsmallersize, to-is-prefix, append-notsmallersize1, append-notsmallersize2,
• nat-inf/addeqinf-cancel is used by from-append-add, less-size-from,
• nat-inf/disj-rqui-infty is used by inf-size-from, append-cut1, zero-len, append-from-ge-02, finlen-tolen, finlen-tolen-02, toinf-empty2, from-append-add, append-split, size-from, appendend-equal, toinf-empty, extensionality, less-size-from, size-empty-equiv, swap-to-from-app,
• nat-inf/eq-natinf-to-nat-2-2 is used by size-append,
• nat-inf/inf-less is used by append-toinf-ls, toinf-empty2, from-append-add, toinfto-append-add, less-size-from, size-toinf, from-append-toinffrom,
• nat-inf/inj-rqui is used by zero-len, append-from-ge-02, finlen-tolen, inf-size-to, finlen-tolen-02, size-to-02, size-empty, from-append-add, append-split, size-from, fin-size-from, extensionality, append-split-fin, size-toinf, size-empty-equiv,
• nat-inf/lele-refl is used by append-from-ge-02,
• nat-inf/lele-trans is used by from-append-tofrom, toinf-to-leq,
• nat-inf/lels-trans is used by extensionality-to, from-append-tofrom,
• nat-inf/less-fin is used by get-to, append-le-to, to-from-01, append-from-ge-02, fin-to-to-leq, leq-prefix, fin-to-to-eq, get-append-ls, append-from-gr-02, lslen-fromnotempty, get-toinf, to-unwind-begin, from-append-tofrom, from-append-add, size-from-less, size-from, to-to-leq, to-empty, append-gr-to, to-empty2, size-to, fin-to-to-ls, fin-size-from, extensionality, elim-fromto, from-succ, contractinf-tl, toinf-to-ls, toinf-to-leq, size-succ, contractinf-from1, less-size-from, get-append-notls, to-unwind-end, ton-fromn,
• nat-inf/less-inf1 is used by from-from, size-inf-toinf, swap-inf-from-to, append-from-gr-02, toinf-empty3, from-append-tofrom, from-append-add, size-from-less, elim-fromto-inf, append-gr-to, toinf-empty, toinf-to-leq-inf, swap-inf-to-from-app, size-succ, toinf-to-eq-inf, get-inftoinf, from-append-toinffrom,
• nat-inf/less-inf2 is used by extensionality, from-succ, contractinf-tl, size-succ, contractinf-from1, less-size-from, get-append-notls, to-unwind-end,
• nat-inf/less-succ-leq is used by size-succ, to-unwind-end,
• nat-inf/ls-le is used by to-is-prefix,
• nat-inf/ls-lsadd is used by from-append-tofrom, size-from-less,
• nat-inf/ls-natinf-to-nat-1-2 is used by from-append-tofrom, size-from-less, swap-to-from-app, to-append-add,
• nat-inf/ls-natinf-to-nat-2-1 is used by from-append-tofrom, get-from, less-size-from,
• nat-inf/ls-natinf-to-nat-2-2 is used by from-append-tofrom,
• nat-inf/ls-notlssucc is used by nlslen-lslensn-eqlensn,
• nat-inf/ls-one is used by to-empty4,
• nat-inf/lsle-trans is used by extensionality-to, get-toinf, toinf-to-ls,
• nat-inf/prime-add-fin is used by swap-to-from-app,
• nat-inf/sel-rqui-dotn is used by append-from-ge-02, append-from-gr-02, from-append-add, size-from, fin-size-from, contractinf-tl, contractinf-from1, get-append-notls, swap-to-from-app,
• nat-inf/zerols-neqzero is used by zero-len, from-to-exchange,

Used from specification stream-basic

• stream-basic/disj-rqui-rqui0 is used by neq-fin-inf-03,
• stream-basic/inj-rqui is used by append-empty-01, eq-stream-to-list-2-1, eq-stream-to-list-2-2, eq-stream-to-list-3-2, fin-empty,
• stream-basic/inj-rqui0 is used by append-fin-inf-fun, cons-eq,
• stream-basic/sel-rqui-dotl is used by extract-empty,
• stream-basic/disj-rqui-rqui0 is used by append-fin-is-inf, fun-nonempty, cons-eq-inf, neq-fin-inf-03, neq-fin-inf-01, appfin-sel, inf-not-toinf-exceptinf, appfin-sel-01, inf-not-to, cons-eq, append-two-is-fin, not-prefix-inf-fin,
• stream-basic/elim-finp-ant is used by from-append-add, appendend-equal, fin-size-from,
• stream-basic/elim-finp-suc is used by from-append-add, appendend-equal, appfin-sel, appfin-sel-01,
• stream-basic/elim-rqui is used by appfin-sel, appfin-sel-01,
• stream-basic/inj-rqui is used by cons-eq-01, from-from, toinflen, append-cancel-l-02, finlen-tolen, from-infto-exchange, append-toinf-ls, toinf-to-eq, from-succ-cons, append-split, empty-append, from-zero, tl-lem, extensionality, tl-fin-1, cons-eq, append-split-fin, append-empty,
• stream-basic/inj-rqui0 is used by from-from, append-cut1, to-plus-from-inf-simp, append-eq-inf, prefix-inf-inf-equal, cons-eq-inf, expand-cons, intrace-expand, toinflen, append-cancel-l-02, elim-hd-tl, from-cons-one, from-succ-cons, append-split, append-assoc, neq-fin-inf-03, cons-append, empty-append, inf-not-toinf-exceptinf, from-zero, elim-fromto-inf, tl-lem, extensionality, from-succ, cons-eq, append-empty, tl-inf-1, appinf-selfun,
• stream-basic/sel-rqui-dotl is used by finlen-tolen, finlen-tolen-02, append-gr-to, append-prefix-fin-is-fin, append-two-is-fin, to-append-add,
• stream-basic/sel-rqui0-dotf is used by append-fin-is-inf, appinf-get-ge, appinf-one2-to-succ, appinf-to-split, appinf-get-le, appinf-sel, appinf-get-ge-01, elim-fromto-inf, appinf-one2-to-succ2, appinf-one2-get-succ, appinf-one2-get-succ2, appinf-get-split, appinf-selfun,
• stream-basic/test-finp-rqui is used by append-fin-is-inf, append-cancel-l-02, append-split, append-split-fin, append-prefix-fin-is-fin, append-two-is-fin,
• stream-basic/test-finp-rqui0 is used by append-fin-is-inf, append-cancel-l-02, append-split, append-prefix-fin-is-fin, append-two-is-fin,

Used from specification list-getput

• list-getput/extension is used by infapp-to-ge-01, infapp-to-le, appinf-to-split, from-append-tofrom, infapp-inj, ton-fromn-fin, extensionality, ton-fromn-inf, to-inf-two,
• list-getput/get-zero-01 is used by toone-equal,

Used from specification list-data

• list-data/elim-list-c is used by to-unwind-begin-fin,
• list-data/l is used by to-unwind-begin-fin, zero-len, to-from-01, get-append-ls, infapp-to-le, from-append-add, append-split, append-assoc, infapp-inj, fin-to-to-ls, extensionality, from-succ, infapp-get-ls, infapp-assoc, to-unwind-end, to-unwind-end-fin, size-empty-equiv,
• list-data/size-nil is used by append-from-gt, to-attach, to-all, to-empty-inf, size-empty, from-all, append-split, append-to-le-01, empty-append, infapp-empty, append-from-addsize-01, ton-fromn-fin, append-to-gr-01, ton-fromn-inf, append-from-le-01, size-inf-to,

Used from specification nat-basic

• nat-basic/a is used by append-from-gt, from-succ-cons-l-lem, infapp-get-ge, infapp-to-ge, to-attach, from-from, to-unwind-begin-fin, infapp-one-to-succ2, cons-to-addnum, cons-from-addnum, size-append, to-from-01, from-nf-zero, cons-eq-inf, expand-cons, intrace-expand, extensionality-to, to-unwind-end2, infapp-to-ge-01, get-cons-num, from-from-inf, appinf-one2-to-succ, append-from-gr-01, infapp-to-le, to-all, get-from-zero, to-unwind-begin, appinf-to-split, to-succ-cons-l-lem, from-cons-one, toinf-empty3, from-all, from-succ-cons, from-append-tofrom, from-append-add, infapp-from-gt, append-from-addsize, size-from-less, append-split, append-assoc, cons-to-num, swap-inf-to-from, appinf-one-to-succ, append-to-addsize-01, appinf-get-ge-01, to-to-leq-inf, toinfto-append-add, append-to-le-01, appinf-one-get-succ, append-from-addsize-01, appinf-one2-to-succ2, get-cons-succ, single-to-one, infapp-inj, from-cons-one-fin, appinf-to-ge-01, to-unwind-end-fin2, to-succ2-nf, one-inf, to-succ-cons, append-from-size, appinf-one2-get-succ, tl-lem, appinf-one-to-succ2, get-from-inf-zero, to-succ3-nf, appinf-one2-get-succ2, to-empty3, append-to-gr-01, get-from-01, appinf-one-get-succ2, infapp-from-le, get-infto, from-to-exchange, from-succ, cons-eq, to-inf-one, swap-inf-to-from-app, append-from-le-01, swap-to-from, infapp-get-eqadd, tl-inf-1, to-inf-two, infapp-assoc, contractinf-from1, less-size-from, cons-from-num, infapp-to-eqadd, get-append-notls, to-unwind-end, to-unwind-end-inf2, to-unwind-end-fin, infapp-one-to-succ, append-from-size-01, swap-to-from-app, from-append-toinffrom, to-append-add, size-inf-to, to-unwind-end-inf,
• nat-basic/add-base is used by append-from-gt, to-attach, infapp-one-to-succ2, from-nf-zero, cons-eq-inf, get-from-zero, from-cons-one, cons-to-num, appinf-one-to-succ, append-to-addsize-01, append-to-le-01, appinf-one-get-succ, append-from-addsize-01, get-cons-succ, appinf-to-ge-01, one-inf, to-succ-cons, append-from-size, get-from-inf-zero, from-to-exchange, from-succ, cons-eq, append-from-le-01, infapp-one-to-succ, append-from-size-01, swap-to-from-app, to-append-add,
• nat-basic/c is used by append-from-gt, from-succ-cons-l-lem, infapp-get-ge, infapp-to-ge, to-attach, from-from, to-unwind-begin-fin, infapp-one-to-succ2, cons-to-addnum, cons-from-addnum, size-append, to-from-01, from-nf-zero, cons-eq-inf, expand-cons, intrace-expand, extensionality-to, to-unwind-end2, infapp-to-ge-01, get-cons-num, from-from-inf, appinf-one2-to-succ, append-from-gr-01, infapp-to-le, to-all, get-from-zero, to-unwind-begin, appinf-to-split, to-succ-cons-l-lem, from-cons-one, toinf-empty3, from-all, from-succ-cons, from-append-tofrom, from-append-add, infapp-from-gt, append-from-addsize, size-from-less, append-split, append-assoc, cons-to-num, swap-inf-to-from, appinf-one-to-succ, append-to-addsize-01, appinf-get-ge-01, to-to-leq-inf, toinfto-append-add, append-to-le-01, appinf-one-get-succ, append-from-addsize-01, appinf-one2-to-succ2, get-cons-succ, single-to-one, infapp-inj, from-cons-one-fin, appinf-to-ge-01, to-unwind-end-fin2, to-succ2-nf, one-inf, to-succ-cons, append-from-size, appinf-one2-get-succ, get-from, tl-lem, appinf-one-to-succ2, get-from-inf-zero, to-succ3-nf, appinf-one2-get-succ2, to-empty3, append-to-gr-01, get-from-01, appinf-one-get-succ2, infapp-from-le, get-infto, from-to-exchange, from-succ, cons-eq, to-inf-one, swap-inf-to-from-app, append-from-le-01, swap-to-from, infapp-get-eqadd, tl-inf-1, to-inf-two, infapp-assoc, contractinf-from1, less-size-from, cons-from-num, infapp-to-eqadd, get-append-notls, to-unwind-end, to-unwind-end-inf2, to-unwind-end-fin, infapp-one-to-succ, append-from-size-01, get-from-inf, swap-to-from-app, from-append-toinffrom, to-append-add, size-inf-to, to-unwind-end-inf,
• nat-basic/eq-01 is used by infapp-to-ge-01, from-append-tofrom, append-split, size-inf-to,
• nat-basic/f is used by append-from-gt, to-unwind-begin-fin, get-to, to-from-01, infapp-to-ge-01, to-to-ls, get-append-ls, append-from-gr-01, infapp-to-le, appinf-to-split, from-append-tofrom, from-append-add, append-assoc, to-to-leq-inf, infapp-inj, append-to-gr-01, fin-to-to-ls, extensionality, get-infto, from-succ, infapp-get-ls, to-inf-two, infapp-assoc, to-unwind-end, to-unwind-end-fin,
• nat-basic/l is used by from-append-tofrom, from-append-add, append-to-gr-01, infapp-from-le, infapp-assoc,
• nat-basic/l-01 is used by append-from-gt, appinf-to-split, from-append-tofrom, infapp-from-gt, append-to-gr-01, swap-to-from-app,
• nat-basic/l-02 is used by infapp-to-le, from-append-tofrom, from-append-add, infapp-from-gt, append-assoc, appinf-get-ge-01, infapp-inj, appinf-to-ge-01, infapp-get-eqadd, infapp-assoc, get-append-notls, swap-to-from-app,
• nat-basic/less-zero is used by to-unwind-begin, empty-append, infapp-empty, ton-fromn-fin, get-infto, ton-fromn-inf, to-unwind-end,
• nat-basic/lf-01 is used by to-to-leq-inf, infapp-inj, extensionality,
• nat-basic/ls-02 is used by less-size-from,
• nat-basic/nls-fst is used by appinf-one-get-succ,
• nat-basic/one-01 is used by infapp-one-to-succ2, cons-eq-inf, appinf-one-to-succ, cons-append, hd-lem, tl-lem, get-infto, contractinf-tl, cons-eq, to-inf-two, contractinf-from1, infappone-zero, infapp-one-to-succ,
• nat-basic/oz is used by infapp-one-to-succ2, cons-eq-inf, expand-cons, intrace-expand, from-cons-one, from-succ-cons, append-split, to-to-leq-inf, get-cons-succ, one-inf, to-succ-cons, tl-lem, append-to-gr-01, get-infto, from-succ, cons-eq, tl-inf-1, contractinf-from1, to-unwind-end, infapp-one-to-succ,
• nat-basic/pred is used by from-succ-cons,
• nat-basic/refl-Nat is used by leq-prefix, infapp-get-eq, append-to-size-01, to-to-leq-inf, ton-fromn-fin, ton-fromn-inf,
• nat-basic/s-04 is used by to-from-01, to-to-leq-inf, get-infto, from-succ, to-unwind-end-fin,
• nat-basic/succ is used by append-from-gt, to-attach, to-from-01, to-all, elim-hd-tl, from-all, to-to-leq-inf, append-to-le-01, append-from-addsize-01, tl-lem, append-to-gr-01, get-infto, from-to-exchange, from-succ, contractinf-tl, append-from-le-01, tl-inf-1, to-inf-two, to-unwind-end, to-unwind-end-fin, size-inf-to, to-unwind-end-inf,
• nat-basic/z-01 is used by to-empty3,
• nat-basic/z-02 is used by tl-lem, tl-inf-1,

Used from specification list

• list/c is used by from-succ-cons-l-lem, hd-fin-lem, to-succ-cons-l-lem, tl-fin-lem, tl-fin-1,
• list/c-06 is used by append-split,
• list/Nil is used by append-from-gt, to-attach, empty-append, append-to-gr-01, to-unwind-end, to-unwind-end-fin, to-unwind-end-inf,
• list/a is used by append-from-gt, append-empty-01, from-succ-cons-l-lem, infapp-to-ge, appinf-to-ge, to-attach, cons-eq-01, to-unwind-begin-fin, infapp-one-to-succ2, eq-stream-to-list-2-1, cons-to-addnum, size-append, to-plus-from-fin, to-from-01, expand-cons, extensionality-to, infapp-to-ge-01, append-cancel-l-02, get-append-ls, appinf-one2-to-succ, infapp-to-le, to-all, to-unwind-begin, appinf-to-split, elim-hd-tl, to-succ-cons-l-lem, get-cons-zero, from-all, from-succ-cons, from-append-tofrom, from-append-add, append-from-addsize, append-split, append-assoc, cons-to-num, eq-stream-to-list-3-2, eq-stream-to-list-3-1, appinf-one-to-succ, append-to-addsize-01, append-from-le, to-to-leq-inf, toinfto-append-add, cons-append, eq-stream-to-list-3-3, append-to-le-01, empty-append, append-from-addsize-01, append-gr-to, appinf-one2-to-succ2, get-cons-succ, single-to-one, from-cons-one-fin, appinf-to-ge-01, infapp-from-eqadd, to-succ-cons, append-from-size, get-append3-fin, appinf-one-to-succ2, append-to-gr-01, infapp-from-le, tl-fin-1, get-infto, elim-fromto, from-to-exchange, from-succ, cons-eq, to-inf-one, append-from-le-01, append-empty, toone-cons-fin, to-inf-two, infapp-assoc, append-two-is-fin, infapp-to-eqadd, prefix-bothfin-listprefix, get-append-notls, prefix-appendbothfin-listprefix, toone-cons, to-unwind-end, to-unwind-end-fin, infapp-one-to-succ, constrrew, to-append-add, size-inf-to, to-unwind-end-inf,
• list/app is used by appinf-one-to-succ, append-to-addsize-01, single-to-one, to-inf-one, append-empty, toone-cons-fin, toone-cons, to-unwind-end, to-unwind-end-fin, to-append-add,
• list/app-02 is used by append-empty-01, to-from-01, from-succ, to-unwind-end-fin,
• list/app-04 is used by appinf-to-ge, append-cancel-l-02,
• list/app-06 is used by extensionality-to,
• list/c is used by append-from-gt, from-succ-cons-l-lem, to-attach, to-unwind-begin-fin, infapp-one-to-succ2, cons-to-addnum, to-from-01, expand-cons, to-all, to-unwind-begin, elim-hd-tl, to-succ-cons-l-lem, from-all, append-split, cons-append, append-to-le-01, append-from-addsize-01, single-to-one, to-succ2-nf, to-succ-cons, to-succ3-nf, append-to-gr-01, tl-fin-1, get-infto, from-succ, to-inf-one, append-from-le-01, to-unwind-end, to-unwind-end-fin, infapp-one-to-succ, constrrew, size-inf-to, to-unwind-end-inf,
• list/c-03 is used by cons-eq-01,
• list/c-04 is used by toone-equal, toone-one, appinf-one-to-succ, single-to-one, toone-cons-fin, toone-cons, to-unwind-end, to-unwind-end-fin, to-unwind-end-inf,
• list/c-06 is used by cons-eq,
• list/e is used by to-from-01, cons-empty, from-succ, to-unwind-end-fin,
• list/e-01 is used by expand-cons, append-to-gr-01,
• list/in-15 is used by extensionality-to, to-unwind-end,
• list/len is used by size-append, infapp-to-ge-01, infapp-to-le, appinf-to-split, from-append-tofrom, from-append-add, append-split, append-assoc, infapp-from-eqadd, infapp-from-le, infapp-assoc,
• list/len-01 is used by infapp-to-ge, to-attach, to-unwind-begin-fin, infapp-one-to-succ2, cons-to-addnum, appinf-one2-to-succ, to-all, to-unwind-begin, to-succ-cons-l-lem, append-split, cons-to-num, append-to-addsize-01, append-from-le, to-to-leq-inf, append-to-le-01, append-gr-to, appinf-one2-to-succ2, appinf-to-ge-01, to-succ-cons, appinf-one-to-succ2, append-to-gr-01, from-succ, append-two-is-fin, infapp-to-eqadd, prefix-bothfin-listprefix, prefix-appendbothfin-listprefix, to-unwind-end, to-unwind-end-fin, infapp-one-to-succ, to-append-add, to-unwind-end-inf,
• list/len-02 is used by infapp-one-to-succ2, cons-eq-inf, append-split, appinf-one-to-succ, cons-append, appinf-one-get-succ, hd-lem, tl-lem, appinf-one-to-succ2, appinf-one-get-succ2, get-infto, from-to-exchange, contractinf-tl, cons-eq, toone-cons-fin, to-inf-two, contractinf-from1, appinf-one-get-zero, to-unwind-end, infappone-zero, infapp-one-to-succ,
• list/len-05 is used by append-from-gt, to-attach, to-from-01, to-all, from-all, append-to-le-01, append-from-addsize-01, append-to-gr-01, from-succ, append-from-le-01, to-inf-two, to-unwind-end-fin, size-inf-to,

Used from specification list-del

• list-del/first-append is used by to-to-leq-inf,
• list-del/first-append-02 is used by toone-cons-fin,
• list-del/get-append-grt is used by infapp-to-ge-01, from-append-add, get-infto,
• list-del/get-append-less is used by from-append-tofrom,
• list-del/get-numrec is used by from-succ,
• list-del/elim-firstn-restn is used by infapp-to-le, to-plus-from-fin-simp, infapp-from-le,
• list-del/first-length is used by length-to,
• list-del/firstN-empty is used by to-empty-fin, to-empty-fin2,
• list-del/firstN-zero is used by to-attach, to-from-01, to-all, to-empty-fin, to-empty-fin2, to-to-leq-inf, append-to-le-01, single-to-one, to-zero, toone-cons-fin, toone-cons, to-unwind-end-fin,
• list-del/firstn-app is used by to-to-leq-inf,
• list-del/firstn-firstn is used by to-to-leq,
• list-del/firstn-one is used by toone-cons-fin,
• list-del/firstn-one-01 is used by toone-equal,
• list-del/get-append-grt is used by appinf-to-split, from-append-tofrom, append-assoc,
• list-del/get-append-grt-02 is used by infapp-from-le, infapp-assoc, get-append-notls,
• list-del/get-append-less is used by infapp-to-ge-01, get-append-ls, infapp-to-le, appinf-to-split, from-append-add, append-assoc, get-infto, infapp-assoc,
• list-del/get-firstn is used by get-finto,
• list-del/get-succ is used by get-cons-succ, to-inf-two, to-unwind-end-fin,
• list-del/get-zero is used by get-cons-zero, from-succ, to-inf-two, to-unwind-end-fin,
• list-del/one-03 is used by infapp-one-to-succ2, cons-eq-inf, cons-append, hd-lem, tl-lem, get-infto, contractinf-tl, cons-eq, to-inf-two, contractinf-from1, appinf-one-get-zero, infappone-zero, infapp-one-to-succ,
• list-del/rest-empty is used by from-all,
• list-del/rest-len is used by length-from,
• list-del/restN-zero is used by to-from-01, from-all, from-zero, from-cons-one-fin, append-from-size, from-to-exchange, from-succ, append-from-le-01,
• list-del/restn-app is used by append-from-addsize,
• list-del/restn-apprec is used by from-from,
• list-del/restn-at is used by get-from-01,
• list-del/restn-nonempty-2 is used by lslen-fromnotempty,

Used from specification list-last

• list-last/prefix is used by prefix-bothfin-listprefix, prefix-appendbothfin-listprefix,