Make sym-blocks constructible congruent

[bvssvni]

Currently, there is no common axiom scheme for normal and tautological congruence of sym-blocks.

This means that the user needs to add edge case axioms.

In order to avoid this, an axiom scheme should be designed such that congruence of sym-blocks is constructible.

Examples

• nat_add_zero_left_cong : true -> cong'(sym(a, add'(z', a') == a'))

Basic operations

• &
• =>
• |

[bvssvni]

I added a new axiom in #247:

sym_fun_eq : true -> sym(a, f(a')) == f

[bvssvni]

An idea:

cong'(f) -> cong'(sym(a, f(a') == b))