Fixing the errors caused by removing SMTPat on commutativity
Fixing the errors caused by removing SMTPat on commutativity

A-Manning/FStar,FStarLang/FStar,A-Manning/FStar,FStarLang/FStar,A-Manning/FStar,FStarLang/FStar