Coq to Why3: Proof of aux lemma of function correction

Hi! I know this probably isn’t the right place to ask this, but I can’t get an answer at stackOverflow and Why3 doesn’t really have a community or an easy way to ask questions…

So I have this proof in 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.

And I have the same one in 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

But, for some reason, Why3 can’t seem to prove it… Is there a way to sort of “translate” Coq’s proof into Why3 “language”?

Thank you!