@@ -10,7 +10,7 @@ using (xs : List a, ys : List a, G : List (List a))
11 data Elem : a -> List a -> Type where
11 data Elem : a -> List a -> Type where
12 Stop : Elem x (x :: xs)
12 Stop : Elem x (x :: xs)
13− Pop : Elem x ys -> Elem x (y :: xs)
13+ Pop : Elem x ys -> Elem x (y :: ys)
15-- Expr is a reflection of a list, indexed over the concrete list,
15-- Expr is a reflection of a list, indexed over the concrete list,
16-- and over a set of list variables.
16-- and over a set of list variables.