[ cleanup ] Use So and All from base in tests

Author: spcfox

tests/idris2/with/with012/WithProof0ElabFail.idr

@@ -1,5 +1,7 @@
 module WithProof0ElabFail
 
+import Data.So
+import Data.List.Quantifiers
 import Language.Reflection
 
 %default total
@@ -8,16 +10,6 @@ import Language.Reflection
 
 %hide List.filter
 
-data So : Bool -> Type where
-  Oh : So True
-
-eqToSo : b = True -> So b
-eqToSo Refl = Oh
-
-data All : (0 p : a -> Type) -> List a -> Type where
-  Nil  : All p Nil
-  (::) : {0 xs : List a} -> p x -> All p xs -> All p (x :: xs)
-
 filter : (p : a -> Bool) -> (xs : List a) -> List a
 filter p [] = []
 filter p (x :: xs) with (p x)

tests/idris2/with/with012/WithProof0Fail.idr

@@ -1,19 +1,12 @@
 module WithProof0Fail
 
+import Data.So
+import Data.List.Quantifiers
+
 %default total
 
 %hide List.filter
 
-data So : Bool -> Type where
-  Oh : So True
-
-eqToSo : b = True -> So b
-eqToSo Refl = Oh
-
-data All : (0 p : a -> Type) -> List a -> Type where
-  Nil  : All p Nil
-  (::) : {0 xs : List a} -> p x -> All p xs -> All p (x :: xs)
-
 filter : (p : a -> Bool) -> (xs : List a) -> List a
 filter p [] = []
 filter p (x :: xs) with (p x)