module A;

open import Nat;