add proof got peroperty GHI_equal.
remove old ABC_equal proof attempts
remove admit in property DEF_equal to indicate proof gap
add assertion on stream->size