Agda loop

gistfile1.txt

data _==_ {a} {A : Set a} (x : A) : A → Set a where
  Refl : x == x


data SubList {a : Set} : List a -> List a -> Set where
  Base : SubList Nil Nil
  Keep : forall {x xs ys} -> SubList xs ys -> SubList (Cons x xs) (Cons x ys)
  Drop : forall {y zs ys} -> SubList zs ys -> SubList zs (Cons y ys)


SubListAntiSym' : {a : Set} {xs ys : List a} ->  SubList xs ys -> SubList ys xs -> xs == ys
SubListAntiSym' Base slb = Refl
SubListAntiSym' (Keep sla) slb = SubListAntiSym' (Keep sla) slb
SubListAntiSym' (Drop sla) slb = SubListAntiSym' (Drop sla) slb