Function write_assert 

fn write_assert<T: Types>(
    encoder: &SmtEncoder<T>,
    clause: &HornClause<'_, T>,
    out: &mut impl Write,
) -> Result