Fix VC Function Substitution

[rcosta358]

Description

This PR fixes VC function substitution so function equality premises are removed after they are used to rewrite later premises or the conclusion, similarly to normal VC substitution.

Example

f(x) == 0
f(y) == f(x) + 1

simplified to

f(x) == 0
f(y) == 0 + 1

and now simplifies to 

f(y) == 0 + 1

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

[CatarinaGamboa]

I'm fine if this works. Can you add an issue with this situation so that we know we might still need to fix it down the line?

[rcosta358]

Sure.