import Mod

foo : natexp 4 = 7
foo = Refl