diff --git a/bedrock2/src/bedrock2/MetricSemantics.v b/bedrock2/src/bedrock2/MetricSemantics.v
index 4dbd8f0b2..3d64091cf 100644
--- a/bedrock2/src/bedrock2/MetricSemantics.v
+++ b/bedrock2/src/bedrock2/MetricSemantics.v
@@ -312,121 +312,4 @@ Section WithParams.
     - eassumption.
     - eapply exec.extend_env; eassumption.
   Qed.
-
-  Lemma of_metrics_free_eval_expr: forall m l e v,
-      Semantics.eval_expr m l e = Some v ->
-      forall mc, exists mc', MetricSemantics.eval_expr m l e mc = Some (v, mc').
-  Proof.
-    induction e; cbn; intros;
-      repeat match goal with
-        | H: Some _ = Some _ |- _ => eapply Option.eq_of_eq_Some in H; subst
-        | H: _ = Some _ |- _ => rewrite H
-        | IH: forall _, Some _ = Some _ -> _ |- _ => specialize IH with (1 := eq_refl)
-        | IH: forall _: MetricLog, exists _: MetricLog, eval_expr ?m ?l ?e _ = Some _
-          |- context[eval_expr ?m ?l ?e ?mc] => specialize (IH mc)
-        | |- _ => progress fwd
-        | |- _ => Tactics.destruct_one_match
-        end;
-      eauto.
-  Qed.
-
-  Lemma to_metrics_free_eval_expr: forall m l e mc v mc',
-      MetricSemantics.eval_expr m l e mc = Some (v, mc') ->
-      Semantics.eval_expr m l e = Some v.
-  Proof.
-    induction e; cbn; intros; fwd;
-      repeat match goal with
-        | IH: forall _ _ _, eval_expr _ _ _ _ = _ -> _, H: eval_expr _ _ _ _ = _ |- _ =>
-          specialize IH with (1 := H)
-        | H: _ = Some _ |- _ => rewrite H
-        | |- _ => Tactics.destruct_one_match
-        end;
-    try congruence.
-  Qed.
-
-  Lemma of_metrics_free_eval_call_args: forall m l arges args,
-      Semantics.eval_call_args m l arges = Some args ->
-      forall mc, exists mc', MetricSemantics.eval_call_args m l arges mc = Some (args, mc').
-  Proof.
-    induction arges; cbn; intros.
-    - eapply Option.eq_of_eq_Some in H. subst. eauto.
-    - fwd.
-      eapply of_metrics_free_eval_expr in E. destruct E as (mc' & E). rewrite E.
-      specialize IHarges with (1 := eq_refl). specialize (IHarges mc').
-      destruct IHarges as (mc'' & IH). rewrite IH. eauto.
-  Qed.
-
-  Lemma to_metrics_free_eval_call_args: forall m l arges mc args mc',
-      MetricSemantics.eval_call_args m l arges mc = Some (args, mc') ->
-      Semantics.eval_call_args m l arges = Some args.
-  Proof.
-    induction arges; cbn; intros.
-    - congruence.
-    - fwd.
-      eapply to_metrics_free_eval_expr in E. rewrite E.
-      specialize IHarges with (1 := E0). rewrite IHarges. reflexivity.
-  Qed.
-
-  Context (e: env).
-
-  Lemma of_metrics_free: forall c t m l post,
-      Semantics.exec e c t m l post ->
-      forall mc, MetricSemantics.exec e c t m l mc (fun t' m' l' _ => post t' m' l').
-  Proof.
-    induction 1; intros;
-      repeat match reverse goal with
-        | H: Semantics.eval_expr _ _ _ = Some _ |- _ =>
-            eapply of_metrics_free_eval_expr in H; destruct H as (? & H)
-        | H: Semantics.eval_call_args _ _ _ = Some _ |- _ =>
-            eapply of_metrics_free_eval_call_args in H; destruct H as (? & H)
-        end;
-      try solve [econstructor; eauto].
-  Qed.
-
-  Lemma to_metrics_free: forall c t m l mc post,
-      MetricSemantics.exec e c t m l mc post ->
-      Semantics.exec e c t m l (fun t' m' l' => exists mc', post t' m' l' mc').
-  Proof.
-    induction 1; intros;
-      repeat match reverse goal with
-        | H: eval_expr _ _ _ _ = Some _ |- _ =>
-            eapply to_metrics_free_eval_expr in H
-        | H: eval_call_args _ _ _ _ = Some _ |- _ =>
-            eapply to_metrics_free_eval_call_args in H
-        end;
-      try solve [econstructor; eauto].
-    { econstructor. 1: eauto.
-      intros.
-      eapply Semantics.exec.weaken. 1: eapply H1. all: eauto.
-      cbv beta.
-      clear. firstorder idtac. }
-    { econstructor.
-      1: eapply IHexec.
-      cbv beta. intros.
-      fwd.
-      eapply H1. eassumption. }
-    { econstructor; [ eassumption .. | ].
-      cbv beta. intros. fwd. eapply H3. eassumption. }
-    { econstructor. 1-4: eassumption.
-      cbv beta. intros. fwd. specialize H3 with (1 := H4). fwd. eauto 10. }
-    { econstructor. 1-3: eassumption.
-      intros. specialize H2 with (1 := H3). fwd. eauto. }
-  Qed.
-
-  Lemma of_metrics_free_call: forall f t m args post,
-      Semantics.call e f t m args post ->
-      forall mc, call e f t m args mc (fun t' m' rets _ => post t' m' rets).
-  Proof.
-    unfold call, Semantics.call. intros. fwd. eauto 10 using of_metrics_free.
-  Qed.
-
-  Lemma to_metrics_free_call: forall f t m args mc post,
-      call e f t m args mc post ->
-      Semantics.call e f t m args (fun t' m' rets => exists mc', post t' m' rets mc').
-  Proof.
-    unfold call, Semantics.call. intros. fwd.
-    do 4 eexists. 1: eassumption. do 2 eexists. 1: eassumption.
-    eapply Semantics.exec.weaken. 1: eapply to_metrics_free. 1: eassumption.
-    cbv beta. clear. firstorder idtac.
-  Qed.
 End WithParams.