module HomeworkNine
import HomeworkEight
%default total

remove : Eq a => a -> List a -> List a
remove x = filter (/=x)

data FV : List String -> Exp -> Type where
  FVar : FV [s] (Var s)
  FAbs : FV xs e -> FV (remove s xs) (Abs s e)
  FApp : FV xs e1 -> FV ys e2 -> FV (xs ++ ys) (App e1 e2)

fv1 : FV ["x"] (Var "x")
fv1 = FVar

fv2 : FV ["x"] (Abs "y" (Var "x"))
fv2 = FAbs FVar

fv3 : FV ["x","x"] (App (Var "x") (Var "x"))
fv3 = FApp FVar FVar

fv4 : FV [] (Abs "x" (App (Var "x") (Var "x")))
fv4 = FAbs fv3