test.scala

def lemma_leftIdentity(x: MMap[String, BigInt]): Boolean = {
  (append(empty, x) == x) because {
    assert(append(empty, x) == append(MMap.empty, x))
    assert(append(MMap.empty, x) == MMap.empty.merge(x))
    assert(MMap.empty.merge(x) == MMap{ k: String =>
      M.append(MMap.empty.apply(k), x.apply(k))
    })
    assert(MMap{ k: String =>
      M.append(MMap.empty.apply(k), x.apply(k))
    } == MMap{ k: String =>
      M.append(M.empty, x.apply(k))
    })
    assert(MMap{ k: String =>
      M.append(M.empty, x.apply(k))
    } == MMap{ k: String =>
      M.law_leftIdentity(x.apply(k))
      M.append(M.empty, x.apply(k))
    })
    assert(MMap{ k: String =>
      M.law_leftIdentity(x.apply(k))
      M.append(M.empty, x.apply(k))
    } == MMap{ k: String =>
      x.apply(k)
    })
    assert(MMap{ k: String =>
      x.apply(k)
    } == x)
    check(append(empty, x) == x)
  }
}