Equivalence between LEM and DNE

||| Double negation elimination.
DNE : Type
DNE = (t : Type) -> Not (Not t) -> t

||| The law of the excluded middle.
LEM : Type
LEM = (t : Type) -> Either t (Not t)

||| Proof that double negation elimation implies law of excluded middle.
total dne_implies_lem : DNE -> LEM

||| Proof that the law of excluded middle implies double negation elimination.
total lem_implies_dne : LEM -> DNE

Please log in; otherwise your solution and progress won't be saved