proof: consume right-sub expression helper bridge

[Th0rgal]

Summary

• add named evidence interfaces for the right-helper Expr.sub letVar consumer
• add the spec-functions Stmt.letVar bridge for Expr.sub when the helper payload is in the right operand
• regenerate PrintAxioms for the new public consumer theorem

Validation

• lean-slot lake build Compiler.Proofs.HelperStepProofs
• python3 scripts/check_proof_length.py
• python3 scripts/generate_print_axioms.py
• python3 scripts/generate_print_axioms.py --check
• git diff --check
• rg -n '\bsorry\b|\badmit\b|axiom |True :=|\t' Compiler/Proofs/HelperStepProofs.lean PrintAxioms.lean

[vercel]

The latest updates on your projects. Learn more about Vercel for GitHub.

Project	Deployment	Actions	Updated (UTC)
verity	Ready	Preview, Comment	Jul 11, 2026 8:50am