module SetInf where id : ∀ {A} → A → A id x = x