
  0 | module Algebra.Solver.Ops
  1 | 
  2 | import public Data.List.Elem
  3 | 
  4 | export infixl 8 .+>, <+., .+.
  5 | 
  6 | ||| Checks if elements `x` and `y` are at the same position in list
  7 | ||| `xs` and thus identical.
  8 | public export
  9 | eqElem : (e1 : Elem x xs) -> (e2 : Elem y xs) -> Maybe (e1 ~=~ e2)
 10 | eqElem Here Here      = Just Refl
 11 | eqElem Here (There z) = Nothing
 12 | eqElem (There z) Here = Nothing
 13 | eqElem (There z) (There w) = case eqElem z w of
 14 |   Just Refl => Just Refl
 15 |   Nothing   => Nothing
 16 |