Theorem to-succ-cons-l-lem

• Type: A user defined theorem
• Validity: The proof is valid.
• Features: simp, localsimp,
• Comment:
• Used by: append-to-gr, append-to-le, append-to-le-01, get-finto, length-to, single-to-one, to-all, to-from-01, to-plus-from-fin, to-succ-cons, to-unwind-begin-fin, to-unwind-end-fin,
• Used by units in proved state: mon-lim-filter-count,
• Proof exists?: Yes

View the proof

Infos about the proof

• Proved?: Yes
• Interactions: 2
• Proof steps: 2
• Used lemmas: to-succ-cons-l,
• Used spec theorems:
  • list/c
• Used simplifier rules: