Property of two ANEAs is in NP I have two arbitrary acyclic nondeterministic finite automata $\mathcal{A_1}$ and $\mathcal{A_2}$ and want to show that the problem $L(\mathcal{A_1}) \not \subseteq L(\mathcal{A_2})$ is in NP by specifying a polynomial proof system.

We defined a polynomial proof system in the following way:

For $L \subseteq \Sigma^*$ the relation $R \subseteq \Sigma^* \times \Gamma^*$ is a proof system for $L$ if $(w,b) \in R \Rightarrow w \in L$ and $w \in L \Rightarrow \exists b \in \Gamma^*: (w,b) \in R$. $R$ is polynomial if there is a polynomial $p$ with $|b| \le p(|w|)$ for all $(w,b) \in R$ and $R \in P$.

Unfortunately I have no idea how to get the relation and any help would be appreciated.
Hint: Suppose that $\mathcal{A}_1$ has $n$ states. Since it is acyclic, all the words it accepts have length at most $n-1$ (why?). Therefore if $L(\mathcal{A}_1) \nsubseteq L(\mathcal{A}_2)$ there must exist a word $w$ of length at most $n-1$ that $\mathcal{A}_1$ accepts but $\mathcal{A}_2$ rejects.