∀ (a : String) (a_1 : Std.Net.MACAddr) (a_2 : Bool) (a_3 a_4 b b_1 : Std.Net.IPAddr),
  ¬a_3 = b →
    ¬{ name := a, physicalAddress := a_1, isLoopback := a_2, address := a_3, netMask := a_4 } =
        { name := a, physicalAddress := a_1, isLoopback := a_2, address := b, netMask := b_1 }