@@ -95,6 +95,10 @@ data SubList : List a -> List a -> Type where
9595 SubNil : SubList [] xs
9696 InList : SubElem x ys -> SubList xs ys -> SubList (x :: xs) ys
9797
98+Uninhabited (SubElem x []) where
99+ uninhabited Z impossible
100+ uninhabited (S _) impossible
101+
98102-- Some useful hints for proof construction in polymorphic programs
99103%hint
100104public export total
@@ -150,9 +154,9 @@ envElem Z (x :: xs) = [x]
150154envElem (S k) (x :: xs) = envElem k xs
151155
152156||| make an environment corresponding to a sub-list
153−%assert_total dropEnv : Env m ys -> SubList xs ys -> Env m xs
157+total dropEnv : Env m ys -> SubList xs ys -> Env m xs
154158dropEnv [] SubNil = []
155−-- dropEnv [] (InList y z) impossible
159+dropEnv [] (InList idx rest) = absurd idx
156160dropEnv (y::ys) SubNil = []
157161dropEnv e@(y::ys) (InList idx rest) =
158162 let [x] = envElem idx e