Coq to Why3: Доказательство вспомогательной леммы о коррекции функций

Question

У меня есть это доказательство в Coq:

      Lemma executeCompile : forall (state:M.t Z) (ins:aexp) (p:list insSt) (stack:list Z),
  execute state stack (compile ins ++ p) = execute state ((aeval ins state)::stack) p.
Proof.
  intros state ins. induction ins;intros p stack;simpl.
  - reflexivity. 
  - reflexivity.
  - Check app_assoc_reverse. rewrite app_assoc_reverse. rewrite IHins.
      simpl. reflexivity.
  - rewrite app_assoc_reverse. rewrite IHins1.
      rewrite app_assoc_reverse. rewrite IHins2.
      simpl. reflexivity.
  - rewrite app_assoc_reverse. rewrite IHins1.
      rewrite app_assoc_reverse. rewrite IHins2.
      simpl. reflexivity.
  - rewrite app_assoc_reverse. rewrite IHins1.
      rewrite app_assoc_reverse. rewrite IHins2.
      simpl. reflexivity. 
Qed.

И я должен доказать ту же лемму в Why3:

      lemma compile_correct_aux : forall a : aexp, s  state, st : stack, p : prog.
  execute s st (compile a ++ p) = execute s (Cons (aeval a s) st) p

Но по какой-то причине Why3 не может это доказать ... Есть ли способ как бы «перевести» доказательство Coq на «язык» Why3? (Если требуются дополнительные распечатки или информация, пожалуйста, дайте мне знать)

Спасибо!