fn write_kvar_decl<T: Types>( encoder: &SmtEncoder<T>, kvar: &KVarDecl<T>, out: &mut impl Write, ) -> Result