{motive : Std.Net.InterfaceAddress → Sort u} →
  (t : Std.Net.InterfaceAddress) →
    ((name : String) →
        (physicalAddress : Std.Net.MACAddr) →
          (isLoopback : Bool) →
            (address netMask : Std.Net.IPAddr) →
              motive
                { name := name, physicalAddress := physicalAddress, isLoopback := isLoopback, address := address,
                  netMask := netMask }) →
      motive t