I want to express the following in a computationally less-loaded way:
$\forall i < A [F(i) = B \implies H(i) = C]$
Taking some shortcuts, this says:
For all $i$, if $F(i) = B$, then $H(i)$ should equal $C$.
Considering the following fact, this is making us check too much: $\forall i, j < A [F(i) = F(j) \implies H(i) = H(j)]$. Hence, a computationally more concise way to say the same is:
For the first $i$ satisfying $F(i) = B$, $H(i)$ should equal $C$.
However, the best I can think of for this is very heavy in notation:
$\left|\{i<A:F(i)=B\}\right| >0 \implies H(\min{\{i<A:F(i)=B\}})=C$
Is there a best-of-both-worlds solution to this?
The formula $\forall i<A.F(i)=B\implies H(i)=C$ states that for every instance of $i<A$, if $F(i)=B$ then $H(i)=C$. It is not sufficient to check only the least $i$ such that $F(i)=B$.
Unless $F$ is stated to be a bijection, it may be the case that for the least $i<A$ such that $F(i)=B$, $H(i)=C$, and yet for some $i<j<A$, $F(j)=B$ and $H(j)\ne C$.
For example, say that $A=3$, $B=1$ and $C=4$. If $F(0)=0$, $F(1)=1$, and $F(2)=1$, and $H(0)=0$, $H(1)=4$, and $H(2)=1$, then your formula...
$$\left\vert\{i<A\mid F(i)=B\}\right\vert>0\implies H\left(\min\{i<A\mid F(i)=B\}\right)=C$$
...holds, since both the consequent and antecedent are true (1 is th minimum, and $F(1)=1$ and $H(1)=4$). However, the orignal formula...
$$\forall i<A.F(i)=B\implies H(i)=C$$
...does not, since $F(2)=1$ and $H(2)=1\ne4$.
As far as notation goes, the original formula is about as concise as it can possibly be.
As for making the evaluation of the original formula more computation friendly, this is what I would do:
Let $G(i)=\begin{cases}1&F(i)=B\\0&\text{otherwise}\end{cases}$ and $K(i)=\begin{cases}1&F(i)=B\land H(i)=C\\0&\text{otherwise}\end{cases}$
Then...
$$\forall i<A.F(i)=B\implies H(i)=C\iff i<A\implies G(i)-K(i)=0$$
This works best if you treat $G$ and $K$ as 'vectors' - then $G-K$ is the zero vector. In the above example where $B=1$ and $C=4$, you get $G=(0,1,1)$ and $K=(0,1,0)$.
$$(0,1,1)-(0,1,0)=(0,0,1)\ne(0,0,0),\qquad\therefore \neg(\forall i<A.F(i)=B\implies H(i)=C)$$
By this method, the formula reduces to...
$$\forall i<A.F(i)=B\implies H(i)=C\iff G-K=\mathbf{0}$$
I can't guarantee that there isn't a more computationally efficinet method of checking your formula (there almost certainly is), but this works well enough. If your doing this by hand, you can simplify the process to:
1) write out $F$ in one row
2) write $H$ in a row below it
3) every time you see $B$ in the top row, draw a box around it and the entry below it.
4) continue until you hit a box whose lower entry is not $C$ or you reach the end of the list.
Edit:
OP has clarified that the function $F$ satisfies $\forall i,j<A.F(i)=F(j)\implies H(i)=H(j)$
That being the case, we need only check that if there is at least one $i$ such that $F(i)=B$, then $H(i)=C$. As a first order formula, this is written...
$$\exists i<A.F(i)=B\implies\exists i<A.F(i)=B\land H(i)=C$$
As for an algorithm to evaluate the formula, I'm not sure whether it is more or less efficient to parse $F$ and $H$ through to the first $i$ satisfying the formula, or to treat them as vectors, as above. It may depend on the value of $A$. In either case, the original method can be modified to work with the new formula.
Let $G(i)=\begin{cases}1&F(i)=B\\0&\text{otherwise}\end{cases}$ and $K(i)=\begin{cases}1&F(i)=B\land H(i)=C\\0&\text{otherwise}\end{cases}$.
Then...
$$\exists i<A.F(i)=B\land H(i)=C\iff G=\mathbf{0}\lor K(i)\ne\mathbf{0}$$
By hand...
1) write out $F$ in one row
2) write $H$ in a row below it
3) find the first instance of $B$ in the top row - your formula holds iff the entry below it is $C$ or there are no $B$