Add VC Function Substitution

[rcosta358]

Description

This PR adds VC simplification for exact function invocation equalities through VCImplication chains. When a refinement contains an equality such as f(x) == 0, later occurrences of f(x) in the VC suffix are replaced with 0, while preserving the source equality and simplification origins. Unlike normal binder substitution, this pass does not remove the source node.

Example

∀x:int. f(x) == 0 =>
∀y:int. f(y) == f(x) + 1 =>
f(y) == 1

is simplified to

∀x:int. f(x) == 0 =>
∀y:int. f(y) == 0 + 1 =>
f(y) == 1

with origin ∀x:int. f(x) == 0

Related Issue

None.

Type of change

• Bug fix
• New feature
• Documentation update
• Code refactoring

Checklist

• Added/updated tests
• mvn test passes locally
• Updated docs/README if behavior or API changed