let mk_update a i x =
    assert(Term.is_var a);
    assert(Term.is_var i);
    assert(Term.is_var x);
    update a i x