I'm trying to prove a simple conjecture using JAPE application. There must be some 'magic trick' in JAPE to get rid of double negation statements but I have no idea how to handle it properly. The point where it all makes sens to me is:
I have started from line 5 and then going backwards I did implication intro twice. Could anyone (who knows JAPE) tell me how to get --E to E and from --F to F so the implication E -> F holds?
After Mauro's suggestions I'm at the point were I have a contradiction but JAPE still wants smth more in it: