Moved fromAList into HOL, rearranged some lemmas
Proved Alloc case