diff options
Diffstat (limited to 'backend/Profilingproof.v')
| -rw-r--r-- | backend/Profilingproof.v | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/backend/Profilingproof.v b/backend/Profilingproof.v index abb86bdb..0cebc601 100644 --- a/backend/Profilingproof.v +++ b/backend/Profilingproof.v @@ -112,6 +112,11 @@ Lemma inject_profiling_call_increases: Proof. intros. simpl. + rewrite <- (Pos2Nat.id (Pos.succ (Pos.succ extra_pc))). + rewrite <- (Pos2Nat.id (extra_pc + 2)). + rewrite !Pos2Nat.inj_succ. + rewrite !Pos2Nat.inj_add. + apply f_equal. lia. Qed. |