Ok, if you look at the constraints for the exercise you'll see that you cannot use Ana Con, you can only use into\elim for true and false connectives, identity and quantifiers. The goal implies that you need to proof 2 identities, c = a and b = e. Furthermore, I tried to do =elim in one go based on the identities, but that doesn't work, you can only eliminate 1 identity at a time from the original premise to get to the goal. I'm not going to give you the entire answer because it would probably be defiant to the goal of doing the exercise.
I will give you a hint though, use the first 2 identity premises and prove the apposite identity by using the =intro and =elim rules i.e. a = c --> a = a --> c = a. Do it for both premises. Then construct another step in the proof to eliminate only the first identity from the original between() premise, citing the first premise and the first identity proof, finally you can eliminate the second identity. If you are still stuck, you can mail me.
ferdiel@absa.co.za
P.S. You need a total of 9 steps, including the premises.
