idris-0.11.1: test/reg072/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