IndProp,Maps: fix type issues and regressions

Author: yurrriq

src/IndProp.lidr

@@ -1268,13 +1268,6 @@ by combining evidence for \idr{Not p} with the \idr{ReflectF} constructor.
 It is easy to formalize this intuition and show that the two statements are
 indeed equivalent:
 
-\todo[inline]{Remove when a release with
-https://github.com/idris-lang/Idris-dev/pull/3925 happens}
-
-> implementation Uninhabited (False = True) where
->   uninhabited Refl impossible
->
-
 > iff_reflect : (p <-> (b = True)) -> Reflect p b
 > iff_reflect {b = False} (pb, _) = ReflectF (uninhabited . pb) Refl
 > iff_reflect {b = True} (_, bp) = ReflectT (bp Refl) Refl

src/Maps.lidr

@@ -79,28 +79,13 @@ present purposes you can think of it as just a fancy \idr{Bool}.)
 The following useful property of  \idr{beq_id} follows from an analogous lemma
 about strings:
 
-\todo[inline]{Copied \idr{<->} for now}
-
-> iff : {p,q : Type} -> Type
-> iff {p} {q} = (p -> q, q -> p)
->
-> syntax [p] "<->" [q] = iff {p} {q}
->
-
-\todo[inline]{Remove when a release with
-https://github.com/idris-lang/Idris-dev/pull/3925 happens}
-
-> implementation Uninhabited (False = True) where
->   uninhabited Refl impossible
->
-
 > beq_id_true_iff : (beq_id x y = True) <-> x = y
 > beq_id_true_iff = (bto, bfro)
 >   where
 >     bto : (beq_id x y = True) -> x = y
 >     bto {x=MkId n1} {y=MkId n2} prf with (decEq n1 n2)
 >       bto Refl | Yes eq = cong {f=MkId} eq
->       bto prf  | No _   = absurd prf
+>       bto Refl | No _ impossible
 >
 >     idInj : MkId x = MkId y -> x = y
 >     idInj Refl = Refl