unshadow.idr

data Foo : (x : List a) -> (y : List b) -> Type where
  MkFoo : (bar: a -> b) -> Foo x y

bar : Foo {a} {b} x y -> a -> b
bar (MkFoo _) x' = ?rhs

{-
  b : Type
  a : Type
  y : List b
  x : List a
  x' : a
  b1 : Type
  a1 : Type
  bar : a1 -> b1
--------------------------------------
rhs : b
-}