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

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

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