Theorem eq-stream-to-list-2-1

• Type: A user defined theorem
• Validity: The proof is valid.
• Features: simp, localsimp,
• Comment:
• Used by: append-cancel-l-02, append-cancel-r-02, append-cancel-r-04, elim-fromto, eq-stream-to-list-3-1, from-succ, to-succ-cons, to-unwind-end,
• Used by units in proved state: mon-lim-filter-count, streamseq-mon-lim,
• Proof exists?: Yes

View the proof

Infos about the proof

• Proved?: Yes
• Interactions: 2
• Proof steps: 3
• Used lemmas: append-assoc, eq-stream-to-list-2-2, append-finfin,
• Used spec theorems:
  • stream-basic/inj-02
• Used simplifier rules:
  • list/a