Add rewrite rule for a pecial case of equality between if expressions

[mpetruska]

Description

Added rule:

• (sif h : c then e1 else e2) = (sif h : b then e3 else e4) ==> (c = b) (if e1 =ₚₜᵣ e3 ∧ e2 =ₚₜᵣ e4 ∧ e1 ≠ e2)

Type of Change

• Bug fix (non-breaking change fixing an issue)
• New feature (non-breaking change adding functionality)
• Breaking change (fix or feature causing existing functionality to change)
• Documentation update
• Performance improvement
• Code refactoring
• Test updates

Related Issue

• Closes #615

Changes Made

• Implemented rule.
• Added "not equal" check in Hypotheses.lean to check inequality between expressions.

Testing

Test Coverage

• Added new tests for new functionality
• Updated existing tests
• All tests pass locally
• For bug fixes: Added example to Tests/Issues/ folder

Documentation

• README updated (if applicable)
• Code comments added/updated
• Doc comments added for new optimization/rewritting rules

Checklist

• My code follows the project's style guidelines
• I have performed a self-review of my code
• I have commented my code, particularly in hard-to-understand areas
• I have made corresponding changes to the documentation
• I have added tests that prove my fix is effective or that my feature works
• New and existing unit tests pass locally with my changes using make check_all
• For bug fixes: Original failing example added to Tests/Issues/ folder with reference to issue number