Any advice on how to make step 6 check out?
The problem is you can't conclude
FrontOf(d, e)from step 4, isn't it?
Then isn't another quantifier elimination all you need (i.e. prove that Cube(e) and Dodec(d) implies FrontOf(d, e)) ?
Also I'm wondering if you mixed up the order of e and y in step 4.
Separate names with a comma.