Proof by induction over rules for mutually recursive relations
Yes, it's legit; no, you'll, (usually) have to "merge" the proofs.

You are trying to prove some property of an inductively defined set. You can do so using (structural) induction along the inductive order induced by your definition.

In a nutshell, you'll assume the property for all terms up to "size" (t.b.d.) $n$ (which has to apply to all rule premises) and conclude the property for terms up to size $n+1$ (the conclusions).

In your case, coming up with a good measure of size may be the hardest part, since $a⋅x⇓e$ and $a⋅x↓v$ are of the same "size" if you count operators. What size measure will work is impossible to say without seeing the whole calculus, though. Of course, for structural induction you don't strictly need such a measure; you can just follow the inductive order (see here for examples). As long as your semantics is well-defined, that should work.