idris-0.12.3: test/regression002/DoubleEquality.idr
module DoubleEquality
oops : Void
oops = the ((False = True) -> Void) (\Refl impossible) $ cong {f = (>0) . (1/)} $ the (-0.0 = 0.0) Refl
module DoubleEquality
oops : Void
oops = the ((False = True) -> Void) (\Refl impossible) $ cong {f = (>0) . (1/)} $ the (-0.0 = 0.0) Refl