"Not a valid application of the rule".
I don't think 7 - 8 is something that really needs to be proven beyond a reit, but I feel like you should be able to...
I'm quite confused on proving Cube(a) given the premise. I feel like that's where the main issue is.
Can anyone give me a hint or two on where I'm going wrong?
On line 8 you might try doing what you did on line 6 and eliminate the biconditional on line 2 rather than using reiteration. Besides what you need to somehow derive in this subproof assuming "Dodec(c)" on line 7 is "Cube(a)". By eliminating the biconditional this would give you "Cube(a) ∧ Tet(b)" using lines 2 and 7.
Then on line 9 you could use conjunction elimination to get "Cube(a)" and this gives you what you need for that conditional.
Then on line 10 you could introduction the biconditional using the conditionals from lines 3-6 ("Cube(a) → Dodec(c)") and lines 7-9 ("Dodec(c) → Cube(a)"). This should give you the goal "Cube(a) ↔ Dodec(c)".
On your current line 9, the reason you are getting the error "Not a valid application of the rule" is because you do not have a biconditional on that line but simply "Dodec(c)". You would need something with an "↔" to introduce the biconditional there.
