module Vale.Def.Words.Four_s
open FStar.Mul