diff --git a/bedrock2/src/bedrock2/LeakageWeakestPreconditionProperties.v b/bedrock2/src/bedrock2/LeakageWeakestPreconditionProperties.v
index 13e0e4960..8413317e5 100644
--- a/bedrock2/src/bedrock2/LeakageWeakestPreconditionProperties.v
+++ b/bedrock2/src/bedrock2/LeakageWeakestPreconditionProperties.v
@@ -21,9 +21,9 @@ Section WeakestPrecondition.
        when trying to use Proper_load, or, due to COQBUG https://github.com/coq/coq/issues/11487,
        we'd get a typechecking failure at Qed time. *)
     repeat match goal with x : ?T |- _ => first
-      [  constr_eq T X; move x before pick_sp
-       | constr_eq T X; move x before ext_spec
-       | constr_eq T X; move x before locals
+      [  constr_eq x pick_sp
+       | constr_eq x ext_spec
+       | constr_eq x locals
        | constr_eq T X; move x at top
        | revert x ] end;
     match goal with x : X |- _ => induction x end;
@@ -83,6 +83,30 @@ Section WeakestPrecondition.
   Context {locals_ok : map.ok locals}.
   Context {ext_spec_ok : LeakageSemantics.ext_spec.ok ext_spec}.
 
+  Ltac ind_on X ::=
+    intros;
+    (* Note: Comment below dates from when we were using a parameter record p *)
+    (* Note: "before p" means actually "after p" when reading from top to bottom, because,
+       as the manual points out, "before" and "after" are with respect to the direction of
+       the move, and we're moving hypotheses upwards here.
+       We need to make sure not to revert/clear p, because the other lemmas depend on it.
+       If we still reverted/cleared p, we'd get errors like
+       "Error: Proper_load depends on the variable p which is not declared in the context."
+       when trying to use Proper_load, or, due to COQBUG https://github.com/coq/coq/issues/11487,
+       we'd get a typechecking failure at Qed time. *)
+    repeat match goal with x : ?T |- _ => first
+      [  constr_eq x ext_spec_ok
+       | constr_eq x locals_ok
+       | constr_eq x mem_ok
+       | constr_eq x word_ok
+       | constr_eq x pick_sp
+       | constr_eq x ext_spec
+       | constr_eq x locals
+       | constr_eq T X; move x at top
+       | revert x ] end;
+    match goal with x : X |- _ => induction x end;
+    intros.
+
   Global Instance Proper_cmd :
     Proper (
      (pointwise_relation _ (
@@ -112,7 +136,7 @@ Section WeakestPrecondition.
     { destruct H1 as (?&?&?&?). eexists. eexists. split.
       { eapply Proper_expr; eauto; cbv [pointwise_relation Basics.impl]; eauto. }
       { intuition eauto 6. } }
-    { eapply H4; eauto. simpl. intros. eauto. }
+    { match goal with h : _ |- _ => solve [eapply h; eauto; simpl; intros; eauto] end. }
     { eapply LeakageSemantics.exec.weaken; eassumption. }
     { destruct H1 as (?&?&?&?). eexists. eexists. split.
       { eapply Proper_list_map'; eauto; try exact H4; cbv [respectful pointwise_relation Basics.impl]; intuition eauto 2.
diff --git a/bedrock2/src/bedrock2/MetricWeakestPreconditionProperties.v b/bedrock2/src/bedrock2/MetricWeakestPreconditionProperties.v
index 287e4eca3..842b0192e 100644
--- a/bedrock2/src/bedrock2/MetricWeakestPreconditionProperties.v
+++ b/bedrock2/src/bedrock2/MetricWeakestPreconditionProperties.v
@@ -22,8 +22,8 @@ Section MetricWeakestPrecondition.
        when trying to use Proper_load, or, due to COQBUG https://github.com/coq/coq/issues/11487,
        we'd get a typechecking failure at Qed time. *)
     repeat match goal with x : ?T |- _ => first
-       [ constr_eq T X; move x before ext_spec
-       | constr_eq T X; move x before locals
+       [ constr_eq x ext_spec
+       | constr_eq x locals
        | constr_eq T X; move x at top
        | revert x ] end;
     match goal with x : X |- _ => induction x end;
@@ -72,6 +72,29 @@ Section MetricWeakestPrecondition.
   Context {locals_ok : map.ok locals}.
   Context {ext_spec_ok : Semantics.ext_spec.ok ext_spec}.
 
+  Ltac ind_on X ::=
+    intros;
+    (* Note: Comment below dates from when we were using a parameter record p *)
+    (* Note: "before p" means actually "after p" when reading from top to bottom, because,
+       as the manual points out, "before" and "after" are with respect to the direction of
+       the move, and we're moving hypotheses upwards here.
+       We need to make sure not to revert/clear p, because the other lemmas depend on it.
+       If we still reverted/cleared p, we'd get errors like
+       "Error: Proper_load depends on the variable p which is not declared in the context."
+       when trying to use Proper_load, or, due to COQBUG https://github.com/coq/coq/issues/11487,
+       we'd get a typechecking failure at Qed time. *)
+    repeat match goal with x : ?T |- _ => first
+       [ constr_eq x ext_spec
+       | constr_eq x locals
+       | constr_eq x word_ok
+       | constr_eq x mem_ok
+       | constr_eq x locals_ok
+       | constr_eq x ext_spec_ok
+       | constr_eq T X; move x at top
+       | revert x ] end;
+    match goal with x : X |- _ => induction x end;
+    intros.
+
   Global Instance Proper_cmd :
     Proper 
         (pointwise_relation _ (
diff --git a/bedrock2/src/bedrock2/WeakestPreconditionProperties.v b/bedrock2/src/bedrock2/WeakestPreconditionProperties.v
index 2dad44228..7eded0de4 100644
--- a/bedrock2/src/bedrock2/WeakestPreconditionProperties.v
+++ b/bedrock2/src/bedrock2/WeakestPreconditionProperties.v
@@ -21,8 +21,8 @@ Section WeakestPrecondition.
        when trying to use Proper_load, or, due to COQBUG https://github.com/coq/coq/issues/11487,
        we'd get a typechecking failure at Qed time. *)
     repeat match goal with x : ?T |- _ => first
-       [ constr_eq T X; move x before ext_spec
-       | constr_eq T X; move x before locals
+       [ constr_eq x ext_spec
+       | constr_eq x locals
        | constr_eq T X; move x at top
        | revert x ] end;
     match goal with x : X |- _ => induction x end;
@@ -69,6 +69,28 @@ Section WeakestPrecondition.
   Context {locals_ok : map.ok locals}.
   Context {ext_spec_ok : Semantics.ext_spec.ok ext_spec}.
 
+  Ltac ind_on X ::=
+    intros;
+    (* Note: Comment below dates from when we were using a parameter record p *)
+    (* Note: "before p" means actually "after p" when reading from top to bottom, because,
+       as the manual points out, "before" and "after" are with respect to the direction of
+       the move, and we're moving hypotheses upwards here.
+       We need to make sure not to revert/clear p, because the other lemmas depend on it.
+       If we still reverted/cleared p, we'd get errors like
+       "Error: Proper_load depends on the variable p which is not declared in the context."
+       when trying to use Proper_load, or, due to COQBUG https://github.com/coq/coq/issues/11487,
+       we'd get a typechecking failure at Qed time. *)
+    repeat match goal with x : ?T |- _ => first
+       [ constr_eq x ext_spec
+       | constr_eq x locals
+       | constr_eq x word_ok
+       | constr_eq x locals_ok
+       | constr_eq x ext_spec_ok
+       | constr_eq T X; move x at top
+       | revert x ] end;
+    match goal with x : X |- _ => induction x end;
+    intros.
+
   Global Instance Proper_cmd :
     Proper (
      (pointwise_relation _ (
diff --git a/compiler/src/compiler/ForeverSafe.v b/compiler/src/compiler/ForeverSafe.v
index 51ccb73ee..464054105 100644
--- a/compiler/src/compiler/ForeverSafe.v
+++ b/compiler/src/compiler/ForeverSafe.v
@@ -89,7 +89,10 @@ Section ForeverSafe.
       runsTo (mcomp_sat (run1 iset)) st safe1 ->
       mcomp_sat (run1 iset) st (fun st' => runsTo (mcomp_sat (run1 iset)) st' safe1).
   Proof.
-    induction 1; rename P into safe1.
+    (* avoid induction generalizing safe1 which prevents using run_pong
+       alternative: pose proof run_pong before induction then use the resulting hyp *)
+    remember safe1 as safe1' eqn:E in |-*. apply eq_sym in E.
+    induction 1; rename P into safe1'; subst safe1'.
     - pose proof (run_1_2 _ H) as P. inversion P.
       + exfalso. eapply exclusive; eauto.
       + eapply mcomp_sat_weaken. 2: eassumption.
@@ -98,7 +101,7 @@ Section ForeverSafe.
     - eapply mcomp_sat_weaken. 2: eassumption.
       intros.
       eapply H0. assumption.
-  Fail Qed. Abort. (* TODO report *)
+  Succeed Qed. Abort.
 
   (* one step of invariant preservation: *)
   Lemma runsTo_safe1_inv: forall (st: RiscvMachineL),