set_option relaxedAutoImplicit false
instance has_arr : HasArr Preorder := { Arr := Function }

def foo : Nat := { first := 10 }
