proofs(Layer 1.0 follow-up): stripIsIdentityOnStrippedBody — slash-slash closure #113

Context

PR #111 landed the Layer 1.0 foundation for line-comment stripping:

• stripLineCommentBody + stripLineComments total Idris2 definitions mirroring src/assail/analyzer.rs:931.
• IsStrippedBody shape predicate + stripBodyProducesStrippedShape lemma (Qed).
• Base cases of stripLineCommentsIdempotent (empty + non-slash-headed input) (Qed).
• 3 concrete sanity tests (Refl).

What's open

The slash-slash inductive case of stripLineCommentsIdempotent requires:

stripIsIdentityOnStrippedBody :
    (xs : List Char) -> IsStrippedBody xs ->
    stripLineComments xs = xs

Three constructor cases:

• StripEmpty → Refl
• StripJustNl tail → requires a second induction on tail (arbitrary content)
• StripSpaceCons rest _ → unfold strip on sp + IH

Once that lemma is closed, the slash-slash case of the main theorem is cong (sp :: sp ::) (bodyOutputIdempotent rest).

Acceptance

• No believe_me / assert_total / holes.
• All existing PR proofs(Layer 1.0): Idris2 stripping foundation — base cases + shape lemma #111 tests still pass.
• PROOF-NEEDS.md 'What Still Needs Proving' Layer-1.0 row for this obligation gets moved to 'Completed Proofs'.

Refs

• PROOF-PROGRAMME.md row 1 (Layer 1.0)
• PR proofs(Layer 1.0): Idris2 stripping foundation — base cases + shape lemma #111 (the foundation)
• src/abi/Stripping.idr (the file to extend)