why3 - 長さがゼロの場合の array_eq_sub の動作

Question

に次の補題がありますwhy3。

lemma trivial:
  forall a : array 'a, b : array 'a.
  array_eq_sub a b 0 0

これは基本的なケースの動作のようですが、明らかにそうではありません。これが機能しない理由についてのアイデアはありますか?

更新
私は問題を単一の不足している補題に減らすことができました:

lemma array_eq_2:
  forall a : array 'a, b : array 'a.
  map_eq_sub a.elts b.elts 0 0 -> array_eq_sub a b 0 0

ドキュメントarray_eq_subで指定されている の定義を考えると、これも些細なことのようです。証明者が解決策を見つけられないのはなぜですか?