a few lemmas for holSyntaxExtraScript.sml