module ImplicitPatternLeftApplication; f : {A : Type} -> A -> A; f ({x} y) := y; end;