Upstream recent engagement lemmas for keccak

[palinatolmach]

We need to upstream the following lemmas to keccak.md:

    rule [keccak-slots-disjoint]: keccak ( A ) ==Int keccak ( B ) +Int C => false requires notBool C ==Int 0 [simplification, concrete(C), comm]

    rule [keccak-slots-disjoint-ml-l]: { keccak ( A ) #Equals keccak ( B ) +Int C } => #Bottom requires notBool C ==Int 0 [simplification, concrete(C)]
    rule [keccak-slots-disjoint-ml-r]: { keccak ( B ) +Int C #Equals keccak ( A ) } => #Bottom requires notBool C ==Int 0 [simplification, concrete(C)]