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