Add VC Binder Simplification

[rcosta358]

Description

This PR adds VC binder simplification through VCImplication chains. When a binder implication is trivial, it simplifies the VC chain while preserving simplification origins with SimplifiedVCImplication.

It supports the following simplifications:

• ∀x. true => P → P, when x is not used in P
• ∀x. false => P → true
• ∀x. true → true

Example

∀x:int. true => y > 0

is simplified to

y > 0

with origin ∀x:int. y > 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