Lean code

include.lean

class C {α:ℕ → Type} :=
    (myf:α 1 → α 1 → α 1)
    (cx cy:α 1)

variable {α':ℕ → Type}
variable [s1:@C α']

include α'
include s1
def f1 := C.myf (C.cx α') (C.cy α')
def f2 := f1 /- [Lean]
                don't know how to synthesize placeholder
                context:
                α' : ℕ → Type,
                s1 : C
                ⊢ ℕ → Type
                f1 : Π {α' : ℕ → Type} [s1 : C], α' 1] -/
omit s1
omit α'