Prove:
(Proposition (Equal Transitivity): ==⇒=) ,
with no assumptions.
We prove () by the external prover Otter.
().
•
![[Graphics:Images/index_gr_1.gif]](Images/index_gr_1.gif){kind=small}
,
![[Graphics:Images/index_gr_2.gif]](Images/index_gr_2.gif){kind=small}
) by the external prover Otter.![[Graphics:Images/index_gr_3.gif]](Images/index_gr_3.gif){kind=small}
).![[Graphics:Images/index_gr_4.gif]](Images/index_gr_4.gif)