coq - Program Fixpoint の Coq simple

Question

sの戦術のようなものはありsimplますProgram Fixpointか？

特に、次の些細なステートメントをどのように証明できますか?

Program Fixpoint bla (n:nat) {measure n} :=
match n with
| 0 => 0
| S n' => S (bla n')
end.

Lemma obvious: forall n, bla n = n. 
induction n. reflexivity.
(* I'm stuck here. For a normal fixpoint, I could for instance use 
simpl. rewrite IHn. reflexivity. But here, I couldn't find a tactic 
transforming bla (S n) to S (bla n).*)

明らかに、このおもちゃの例には必要ありませんが、手動でProgram Fixpointの終了を証明する必要がある、より複雑な設定で同じ問題に直面しています。Program Fixpoint