This adds a new rule used to elaborate implicity reasoning with equality symmetry. This addresses issue #43 (closed).