JAPE double negation handling

Question

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?

EDIT:

After Mauro's suggestions I'm at the point were I have a contradiction but JAPE still wants smth more in it:

Answer 1

The 'magic trick' in the Natural Deduction proof is to use Double Negation elimination rule :

$\lnot \lnot \varphi \vdash \varphi$.

If not available, you must have a "contradiction" rules; see : Richard Bornat, Proof and Disproof in Formal Logic : An Introduction for Programmers (2005), that is a reference for Jape software, page 43 :

if $\Gamma \vdash \bot$, then $\Gamma \vdash \varphi$ --- contradiction (constructive)

and :

if $\Gamma, \lnot \varphi \vdash \bot$, then $\Gamma \vdash \varphi$ --- contradiction (classical).

---

In this case, they are not necessary :

The derivation is :

1) $E \to F$ --- premise

2) $\lnot \lnot E$ --- assumed [a]

3) $\lnot F$ --- assumed [b]

4) $E$ --- assumed [c]

5) $F$ --- from 1) and 4) by $\to$-elimination

6) $\bot$ --- from 3) and 5) by $\lnot$-elimination

7) $\lnot E$ --- from 4) and 6) by $\lnot$-intro, discharging [c]

8) $\bot$ from 2) and 7) by $\lnot$-elim

9) $\lnot \lnot F$ --- from 3) and 8) by $\lnot$-intro, discharging [b]

10) $\lnot \lnot E \to \lnot \lnot F$ --- from 2) and 9) by $\to$-intro, discharging [a].