diff --git a/src/controller_examples/fluent_controller/fluentbit/proof/helper_invariants/proof.rs b/src/controller_examples/fluent_controller/fluentbit/proof/helper_invariants/proof.rs
index 6080fcfcd..861f0f8c5 100644
--- a/src/controller_examples/fluent_controller/fluentbit/proof/helper_invariants/proof.rs
+++ b/src/controller_examples/fluent_controller/fluentbit/proof/helper_invariants/proof.rs
@@ -961,9 +961,9 @@ pub proof fn lemma_eventually_always_resource_object_only_has_owner_reference_po
 {
     let key = get_request(sub_resource, fb).key;
     let eventual_owner_ref = |owner_ref: Option<Seq<OwnerReferenceView>>| {owner_ref == Some(seq![fb.controller_owner_ref()])};
-    always_weaken_temp(spec, lift_state(object_in_every_resource_update_request_only_has_owner_references_pointing_to_current_cr(sub_resource, fb)), lift_state(FBCluster::every_update_msg_sets_owner_references_as(key, eventual_owner_ref)));
-    always_weaken_temp(spec, lift_state(every_resource_create_request_implies_at_after_create_resource_step(sub_resource, fb)), lift_state(FBCluster::every_create_msg_sets_owner_references_as(key, eventual_owner_ref)));
-    always_weaken_temp(spec, lift_state(resource_object_has_no_finalizers_or_timestamp_and_only_has_controller_owner_ref(sub_resource, fb)), lift_state(FBCluster::object_has_no_finalizers(key)));
+    always_weaken(spec, lift_state(object_in_every_resource_update_request_only_has_owner_references_pointing_to_current_cr(sub_resource, fb)), lift_state(FBCluster::every_update_msg_sets_owner_references_as(key, eventual_owner_ref)));
+    always_weaken(spec, lift_state(every_resource_create_request_implies_at_after_create_resource_step(sub_resource, fb)), lift_state(FBCluster::every_create_msg_sets_owner_references_as(key, eventual_owner_ref)));
+    always_weaken(spec, lift_state(resource_object_has_no_finalizers_or_timestamp_and_only_has_controller_owner_ref(sub_resource, fb)), lift_state(FBCluster::object_has_no_finalizers(key)));
 
     let state = |s: FBCluster| {
         desired_state_is(fb)(s)
@@ -1008,11 +1008,11 @@ pub proof fn lemma_eventually_always_daemon_set_not_exists_or_matches_or_no_more
 {
     let ds_key = get_request(SubResource::DaemonSet, fb).key;
     let make_fn = || make_daemon_set(fb);
-    implies_preserved_by_always_temp(
+    entails_preserved_by_always(
         lift_state(every_resource_create_request_implies_at_after_create_resource_step(SubResource::DaemonSet, fb)),
         lift_state(FBCluster::every_in_flight_create_req_msg_for_this_ds_matches(ds_key, make_fn))
     );
-    valid_implies_trans(
+    entails_trans(
         spec,
         always(lift_state(every_resource_create_request_implies_at_after_create_resource_step(SubResource::DaemonSet, fb))),
         always(lift_state(FBCluster::every_in_flight_create_req_msg_for_this_ds_matches(ds_key, make_fn)))
diff --git a/src/controller_examples/fluent_controller/fluentbit/proof/helper_invariants/unchangeable.rs b/src/controller_examples/fluent_controller/fluentbit/proof/helper_invariants/unchangeable.rs
index 6a6c5a767..ddf06a4fb 100644
--- a/src/controller_examples/fluent_controller/fluentbit/proof/helper_invariants/unchangeable.rs
+++ b/src/controller_examples/fluent_controller/fluentbit/proof/helper_invariants/unchangeable.rs
@@ -151,7 +151,7 @@ pub proof fn lemma_always_object_in_etcd_satisfies_unchangeable(spec: TempPred<F
         object_in_every_update_request_msg_satisfies_unchangeable_induction(sub_resource, fb, s, s_prime);
     }
     init_invariant(spec, FBCluster::init(), next, inv);
-    always_weaken_temp(spec, lift_state(inv), lift_state(object_in_etcd_satisfies_unchangeable(sub_resource, fb)));
+    always_weaken(spec, lift_state(inv), lift_state(object_in_etcd_satisfies_unchangeable(sub_resource, fb)));
 }
 
 pub proof fn object_in_etcd_satisfies_unchangeable_induction(sub_resource: SubResource, fb: FluentBitView, s: FBCluster, s_prime: FBCluster)
diff --git a/src/controller_examples/fluent_controller/fluentbit/proof/liveness/daemon_set_match.rs b/src/controller_examples/fluent_controller/fluentbit/proof/liveness/daemon_set_match.rs
index 43fb69756..ec6b9b451 100644
--- a/src/controller_examples/fluent_controller/fluentbit/proof/liveness/daemon_set_match.rs
+++ b/src/controller_examples/fluent_controller/fluentbit/proof/liveness/daemon_set_match.rs
@@ -58,7 +58,7 @@ pub proof fn lemma_from_after_get_daemon_set_step_to_daemon_set_matches(spec: Te
         &&& s.resources().contains_key(get_request(SubResource::DaemonSet, fb).key)
         &&& pending_req_in_flight_at_after_get_resource_step(SubResource::DaemonSet, fb)(s)
     });
-    or_leads_to_combine_temp(spec, key_not_exists, key_exists, lift_state(sub_resource_state_matches(SubResource::DaemonSet, fb)));
+    or_leads_to_combine(spec, key_not_exists, key_exists, lift_state(sub_resource_state_matches(SubResource::DaemonSet, fb)));
     temp_pred_equality(
         key_not_exists.or(key_exists), lift_state(pending_req_in_flight_at_after_get_resource_step(SubResource::DaemonSet, fb))
     );
@@ -106,7 +106,7 @@ proof fn lemma_from_after_get_daemon_set_step_and_key_exists_to_daemon_set_match
     let post = lift_state(sub_resource_state_matches(SubResource::DaemonSet, fb));
 
     assert_by(spec.entails(daemon_set_matches.leads_to(post)), {
-        valid_implies_implies_leads_to(spec, daemon_set_matches, post);
+        entails_implies_leads_to(spec, daemon_set_matches, post);
     });
 
     assert_by(spec.entails(daemon_set_not_matches.leads_to(post)), {
@@ -177,7 +177,7 @@ proof fn lemma_from_after_get_daemon_set_step_and_key_exists_to_daemon_set_match
         leads_to_trans_n!(spec, daemon_set_not_matches, post1, post2, post);
     });
 
-    or_leads_to_combine_temp(spec, daemon_set_matches, daemon_set_not_matches, post);
+    or_leads_to_combine(spec, daemon_set_matches, daemon_set_not_matches, post);
     temp_pred_equality(daemon_set_matches.or(daemon_set_not_matches), pre);
 }
 
@@ -402,7 +402,7 @@ proof fn lemma_daemon_set_state_matches_at_after_update_daemon_set_step(spec: Te
         &&& helper_invariants::resource_object_only_has_owner_reference_pointing_to_current_cr(SubResource::DaemonSet, fb)(s)
         &&& helper_invariants::daemon_set_in_etcd_satisfies_unchangeable(fb)(s)
     };
-    always_weaken_temp(spec, lift_state(FBCluster::each_object_in_etcd_is_well_formed()), lift_state(resource_well_formed));
+    always_weaken(spec, lift_state(FBCluster::each_object_in_etcd_is_well_formed()), lift_state(resource_well_formed));
     combine_spec_entails_always_n!(
         spec, lift_action(stronger_next),
         lift_action(FBCluster::next()),
@@ -483,7 +483,7 @@ pub proof fn lemma_daemon_set_is_stable(spec: TempPred<FBCluster>, fb: FluentBit
         }
     }
 
-    leads_to_stable_temp(spec, lift_action(stronger_next), p, lift_state(post));
+    leads_to_stable(spec, lift_action(stronger_next), p, lift_state(post));
 }
 
 }
diff --git a/src/controller_examples/fluent_controller/fluentbit/proof/liveness/proof.rs b/src/controller_examples/fluent_controller/fluentbit/proof/liveness/proof.rs
index 83c7d034d..79af0a735 100644
--- a/src/controller_examples/fluent_controller/fluentbit/proof/liveness/proof.rs
+++ b/src/controller_examples/fluent_controller/fluentbit/proof/liveness/proof.rs
@@ -64,7 +64,7 @@ proof fn liveness_proof(fb: FluentBitView)
     unpack_conditions_from_spec(invariants(fb), assumption, true_pred(), always(lift_state(current_state_matches::<FluentBitMaker>(fb))));
     temp_pred_equality(true_pred().and(assumption), assumption);
 
-    valid_implies_trans(
+    entails_trans(
         cluster_spec().and(derived_invariants_since_beginning(fb)), invariants(fb),
         always(lift_state(desired_state_is(fb))).leads_to(always(lift_state(current_state_matches::<FluentBitMaker>(fb))))
     );
@@ -84,7 +84,7 @@ proof fn spec_before_phase_n_entails_true_leads_to_current_state_matches(i: nat,
     spec_of_previous_phases_entails_eventually_new_invariants(i, fb);
     unpack_conditions_from_spec(spec_before_phase_n(i, fb), invariants_since_phase_n(i, fb), true_pred(), always(lift_state(current_state_matches::<FluentBitMaker>(fb))));
     temp_pred_equality(true_pred().and(invariants_since_phase_n(i, fb)), invariants_since_phase_n(i, fb));
-    leads_to_trans_temp(spec_before_phase_n(i, fb), true_pred(), invariants_since_phase_n(i, fb), always(lift_state(current_state_matches::<FluentBitMaker>(fb))));
+    leads_to_trans(spec_before_phase_n(i, fb), true_pred(), invariants_since_phase_n(i, fb), always(lift_state(current_state_matches::<FluentBitMaker>(fb))));
 }
 
 proof fn lemma_true_leads_to_always_current_state_matches(fb: FluentBitView)
@@ -160,13 +160,13 @@ proof fn lemma_true_leads_to_always_state_matches_for_all_resources(fb: FluentBi
         if sub_resource != SubResource::DaemonSet {
             let next_resource = next_resource_after(sub_resource).get_AfterKRequestStep_1();
             lemma_from_after_get_resource_step_to_resource_matches(spec, fb, sub_resource, next_resource);
-            leads_to_trans_temp(
+            leads_to_trans(
                 spec, true_pred(), lift_state(pending_req_in_flight_at_after_get_resource_step(sub_resource, fb)),
                 lift_state(sub_resource_state_matches(sub_resource, fb))
             );
         } else {
             lemma_from_after_get_daemon_set_step_to_daemon_set_matches(spec, fb);
-            leads_to_trans_temp(
+            leads_to_trans(
                 spec, true_pred(), lift_state(pending_req_in_flight_at_after_get_resource_step(SubResource::DaemonSet, fb)),
                 lift_state(sub_resource_state_matches(SubResource::DaemonSet, fb))
             );
@@ -207,9 +207,25 @@ proof fn lemma_from_reconcile_idle_to_scheduled(spec: TempPred<FBCluster>, fb: F
         &&& s.scheduled_reconciles().contains_key(fb.object_ref())
     };
     let input = fb.object_ref();
-    FBCluster::lemma_pre_leads_to_post_by_schedule_controller_reconcile_borrow_from_spec(spec, input, FBCluster::next(), desired_state_is(fb), pre, post);
-    valid_implies_implies_leads_to(spec, lift_state(post), lift_state(post));
-    or_leads_to_combine_temp(spec, lift_state(pre), lift_state(post), lift_state(post));
+    let stronger_pre = |s| {
+        &&& pre(s)
+        &&& desired_state_is(fb)(s)
+    };
+    let stronger_next = |s, s_prime| {
+        &&& FBCluster::next()(s, s_prime)
+        &&& desired_state_is(fb)(s_prime)
+    };
+    always_to_always_later(spec, lift_state(desired_state_is(fb)));
+    combine_spec_entails_always_n!(
+        spec, lift_action(stronger_next),
+        lift_action(FBCluster::next()),
+        later(lift_state(desired_state_is(fb)))
+    );
+    FBCluster::lemma_pre_leads_to_post_by_schedule_controller_reconcile(spec, input, stronger_next, stronger_pre, post);
+    temp_pred_equality(lift_state(pre).and(lift_state(desired_state_is(fb))), lift_state(stronger_pre));
+    leads_to_by_borrowing_inv(spec, lift_state(pre), lift_state(post), lift_state(desired_state_is(fb)));
+    entails_implies_leads_to(spec, lift_state(post), lift_state(post));
+    or_leads_to_combine(spec, lift_state(pre), lift_state(post), lift_state(post));
     temp_pred_equality(lift_state(pre).or(lift_state(post)), lift_state(|s: FBCluster| {!s.ongoing_reconciles().contains_key(fb.object_ref())}));
 }
 
diff --git a/src/controller_examples/fluent_controller/fluentbit/proof/liveness/resource_match.rs b/src/controller_examples/fluent_controller/fluentbit/proof/liveness/resource_match.rs
index 03437ef7c..309851623 100644
--- a/src/controller_examples/fluent_controller/fluentbit/proof/liveness/resource_match.rs
+++ b/src/controller_examples/fluent_controller/fluentbit/proof/liveness/resource_match.rs
@@ -66,12 +66,12 @@ pub proof fn lemma_from_after_get_resource_step_to_resource_matches(
         &&& s.resources().contains_key(get_request(sub_resource, fb).key)
         &&& pending_req_in_flight_at_after_get_resource_step(sub_resource, fb)(s)
     });
-    or_leads_to_combine_temp(spec, key_not_exists, key_exists, lift_state(sub_resource_state_matches(sub_resource, fb)));
+    or_leads_to_combine(spec, key_not_exists, key_exists, lift_state(sub_resource_state_matches(sub_resource, fb)));
     temp_pred_equality(
         key_not_exists.or(key_exists), lift_state(pending_req_in_flight_at_after_get_resource_step(sub_resource, fb))
     );
     if next_resource_after(sub_resource) == after_get_k_request_step(next_resource) {
-        or_leads_to_combine_temp(spec, key_not_exists, key_exists, lift_state(pending_req_in_flight_at_after_get_resource_step(next_resource, fb)));
+        or_leads_to_combine(spec, key_not_exists, key_exists, lift_state(pending_req_in_flight_at_after_get_resource_step(next_resource, fb)));
     }
 }
 
@@ -176,7 +176,7 @@ pub proof fn lemma_from_after_get_resource_step_and_key_not_exists_to_resource_m
     });
 
     assert_by(spec.entails(pre.leads_to(lift_state(sub_resource_state_matches(sub_resource, fb)))), {
-        valid_implies_implies_leads_to(spec, match_and_ok_resp, lift_state(sub_resource_state_matches(sub_resource, fb)));
+        entails_implies_leads_to(spec, match_and_ok_resp, lift_state(sub_resource_state_matches(sub_resource, fb)));
         leads_to_trans_n!(spec, pre, match_and_ok_resp, lift_state(sub_resource_state_matches(sub_resource, fb)));
     });
 
@@ -237,7 +237,7 @@ pub proof fn lemma_from_after_get_resource_step_and_key_not_exists_to_resource_m
                 }
                 temp_pred_equality(tla_exists(known_ok_resp), exists_ok_resp);
             });
-            valid_implies_implies_leads_to(spec, match_and_ok_resp, exists_ok_resp);
+            entails_implies_leads_to(spec, match_and_ok_resp, exists_ok_resp);
             leads_to_trans_n!(spec, pre, match_and_ok_resp, exists_ok_resp, lift_state(next_state));
         });
     }
@@ -339,7 +339,7 @@ proof fn lemma_from_after_get_resource_step_and_key_exists_to_resource_matches(
     });
 
     assert_by(spec.entails(pre.leads_to(lift_state(sub_resource_state_matches(sub_resource, fb)))), {
-        valid_implies_implies_leads_to(spec, match_and_ok_resp, lift_state(sub_resource_state_matches(sub_resource, fb)));
+        entails_implies_leads_to(spec, match_and_ok_resp, lift_state(sub_resource_state_matches(sub_resource, fb)));
         leads_to_trans_n!(spec, pre, match_and_ok_resp, lift_state(sub_resource_state_matches(sub_resource, fb)));
     });
 
@@ -402,7 +402,7 @@ proof fn lemma_from_after_get_resource_step_and_key_exists_to_resource_matches(
                 }
                 temp_pred_equality(tla_exists(known_ok_resp), exists_ok_resp);
             });
-            valid_implies_implies_leads_to(spec, match_and_ok_resp, exists_ok_resp);
+            entails_implies_leads_to(spec, match_and_ok_resp, exists_ok_resp);
             leads_to_trans_n!(spec, pre, match_and_ok_resp, exists_ok_resp, lift_state(next_state));
         });
     }
@@ -538,7 +538,7 @@ proof fn lemma_from_after_get_resource_step_to_after_create_resource_step(spec:
         &&& helper_invariants::every_resource_create_request_implies_at_after_create_resource_step(sub_resource, fb)(s)
         &&& helper_invariants::no_create_resource_request_msg_without_name_in_flight(sub_resource, fb)(s)
     };
-    always_weaken_temp(spec, lift_state(FBCluster::each_object_in_reconcile_has_consistent_key_and_valid_metadata()), lift_state(consistent_key));
+    always_weaken(spec, lift_state(FBCluster::each_object_in_reconcile_has_consistent_key_and_valid_metadata()), lift_state(consistent_key));
     combine_spec_entails_always_n!(
         spec, lift_action(stronger_next),
         lift_action(FBCluster::next()),
@@ -854,7 +854,7 @@ proof fn lemma_from_after_get_resource_step_to_after_update_resource_step(spec:
         &&& helper_invariants::object_in_etcd_satisfies_unchangeable(sub_resource, fb)(s)
         &&& helper_invariants::resource_object_only_has_owner_reference_pointing_to_current_cr(sub_resource, fb)(s)
     };
-    always_weaken_temp(spec, lift_state(FBCluster::each_object_in_etcd_is_well_formed()), lift_state(resource_well_formed));
+    always_weaken(spec, lift_state(FBCluster::each_object_in_etcd_is_well_formed()), lift_state(resource_well_formed));
 
     combine_spec_entails_always_n!(
         spec, lift_action(stronger_next),
@@ -941,7 +941,7 @@ pub proof fn lemma_resource_object_is_stable(spec: TempPred<FBCluster>, sub_reso
         }
     }
 
-    leads_to_stable_temp(spec, lift_action(stronger_next), p, lift_state(post));
+    leads_to_stable(spec, lift_action(stronger_next), p, lift_state(post));
 }
 
 }
diff --git a/src/controller_examples/fluent_controller/fluentbit/proof/liveness/spec.rs b/src/controller_examples/fluent_controller/fluentbit/proof/liveness/spec.rs
index 20912a0a2..c69a93613 100644
--- a/src/controller_examples/fluent_controller/fluentbit/proof/liveness/spec.rs
+++ b/src/controller_examples/fluent_controller/fluentbit/proof/liveness/spec.rs
@@ -75,8 +75,8 @@ pub proof fn spec_of_previous_phases_entails_eventually_new_invariants(i: nat, f
 {
     let spec = spec_before_phase_n(i, fb);
     reveal_with_fuel(spec_before_phase_n, 8);
-    implies_preserved_by_always_temp(lift_state(desired_state_is(fb)), lift_state(FBCluster::desired_state_is(fb)));
-    valid_implies_trans(spec, always(lift_state(desired_state_is(fb))), always(lift_state(FBCluster::desired_state_is(fb))));
+    entails_preserved_by_always(lift_state(desired_state_is(fb)), lift_state(FBCluster::desired_state_is(fb)));
+    entails_trans(spec, always(lift_state(desired_state_is(fb))), always(lift_state(FBCluster::desired_state_is(fb))));
     if i == 1 {
         FBCluster::lemma_true_leads_to_crash_always_disabled(spec);
         FBCluster::lemma_true_leads_to_busy_always_disabled(spec);
diff --git a/src/controller_examples/fluent_controller/fluentbit/proof/liveness/terminate.rs b/src/controller_examples/fluent_controller/fluentbit/proof/liveness/terminate.rs
index 40107251b..ed99f3ce1 100644
--- a/src/controller_examples/fluent_controller/fluentbit/proof/liveness/terminate.rs
+++ b/src/controller_examples/fluent_controller/fluentbit/proof/liveness/terminate.rs
@@ -56,7 +56,7 @@ pub proof fn reconcile_eventually_terminates(spec: TempPred<FBCluster>, fb: Flue
     FBCluster::lemma_reconcile_done_leads_to_reconcile_idle(spec, fb.object_ref());
     temp_pred_equality(lift_state(at_step_state_pred(fb, FluentBitReconcileStep::Done)), lift_state(FBCluster::reconciler_reconcile_done(fb.object_ref())));
     temp_pred_equality(lift_state(at_step_state_pred(fb, FluentBitReconcileStep::Error)), lift_state(FBCluster::reconciler_reconcile_error(fb.object_ref())));
-    valid_implies_implies_leads_to(spec, lift_state(reconcile_idle), lift_state(reconcile_idle));
+    entails_implies_leads_to(spec, lift_state(reconcile_idle), lift_state(reconcile_idle));
 
     // Second, prove that the sub resource that every intermediate steps can lead to reconcile idle.
     lemma_from_after_get_resource_step_to_after_get_next_resource_step_to_reconcile_idle(spec, fb, SubResource::DaemonSet, FluentBitReconcileStep::Done);
diff --git a/src/controller_examples/fluent_controller/fluentbit_config/proof/helper_invariants/proof.rs b/src/controller_examples/fluent_controller/fluentbit_config/proof/helper_invariants/proof.rs
index 999136ad0..d61b13ad4 100644
--- a/src/controller_examples/fluent_controller/fluentbit_config/proof/helper_invariants/proof.rs
+++ b/src/controller_examples/fluent_controller/fluentbit_config/proof/helper_invariants/proof.rs
@@ -842,9 +842,9 @@ pub proof fn lemma_eventually_always_resource_object_only_has_owner_reference_po
 {
     let key = get_request(sub_resource, fbc).key;
     let eventual_owner_ref = |owner_ref: Option<Seq<OwnerReferenceView>>| {owner_ref == Some(seq![fbc.controller_owner_ref()])};
-    always_weaken_temp(spec, lift_state(object_in_every_resource_update_request_only_has_owner_references_pointing_to_current_cr(sub_resource, fbc)), lift_state(FBCCluster::every_update_msg_sets_owner_references_as(key, eventual_owner_ref)));
-    always_weaken_temp(spec, lift_state(every_resource_create_request_implies_at_after_create_resource_step(sub_resource, fbc)), lift_state(FBCCluster::every_create_msg_sets_owner_references_as(key, eventual_owner_ref)));
-    always_weaken_temp(spec, lift_state(resource_object_has_no_finalizers_or_timestamp_and_only_has_controller_owner_ref(sub_resource, fbc)), lift_state(FBCCluster::object_has_no_finalizers(key)));
+    always_weaken(spec, lift_state(object_in_every_resource_update_request_only_has_owner_references_pointing_to_current_cr(sub_resource, fbc)), lift_state(FBCCluster::every_update_msg_sets_owner_references_as(key, eventual_owner_ref)));
+    always_weaken(spec, lift_state(every_resource_create_request_implies_at_after_create_resource_step(sub_resource, fbc)), lift_state(FBCCluster::every_create_msg_sets_owner_references_as(key, eventual_owner_ref)));
+    always_weaken(spec, lift_state(resource_object_has_no_finalizers_or_timestamp_and_only_has_controller_owner_ref(sub_resource, fbc)), lift_state(FBCCluster::object_has_no_finalizers(key)));
 
     let state = |s: FBCCluster| {
         desired_state_is(fbc)(s)
diff --git a/src/controller_examples/fluent_controller/fluentbit_config/proof/liveness/proof.rs b/src/controller_examples/fluent_controller/fluentbit_config/proof/liveness/proof.rs
index da94e3c0a..e65ec0f99 100644
--- a/src/controller_examples/fluent_controller/fluentbit_config/proof/liveness/proof.rs
+++ b/src/controller_examples/fluent_controller/fluentbit_config/proof/liveness/proof.rs
@@ -55,7 +55,7 @@ proof fn liveness_proof(fbc: FluentBitConfigView)
     unpack_conditions_from_spec(invariants(fbc), assumption, true_pred(), always(lift_state(current_state_matches::<FluentBitConfigMaker>(fbc))));
     temp_pred_equality(true_pred().and(assumption), assumption);
 
-    valid_implies_trans(
+    entails_trans(
         cluster_spec().and(derived_invariants_since_beginning(fbc)), invariants(fbc),
         always(lift_state(desired_state_is(fbc))).leads_to(always(lift_state(current_state_matches::<FluentBitConfigMaker>(fbc))))
     );
@@ -75,7 +75,7 @@ proof fn spec_before_phase_n_entails_true_leads_to_current_state_matches(i: nat,
     spec_of_previous_phases_entails_eventually_new_invariants(i, fbc);
     unpack_conditions_from_spec(spec_before_phase_n(i, fbc), invariants_since_phase_n(i, fbc), true_pred(), always(lift_state(current_state_matches::<FluentBitConfigMaker>(fbc))));
     temp_pred_equality(true_pred().and(invariants_since_phase_n(i, fbc)), invariants_since_phase_n(i, fbc));
-    leads_to_trans_temp(spec_before_phase_n(i, fbc), true_pred(), invariants_since_phase_n(i, fbc), always(lift_state(current_state_matches::<FluentBitConfigMaker>(fbc))));
+    leads_to_trans(spec_before_phase_n(i, fbc), true_pred(), invariants_since_phase_n(i, fbc), always(lift_state(current_state_matches::<FluentBitConfigMaker>(fbc))));
 }
 
 proof fn lemma_true_leads_to_always_current_state_matches(fbc: FluentBitConfigView)
@@ -147,9 +147,25 @@ proof fn lemma_from_reconcile_idle_to_scheduled(spec: TempPred<FBCCluster>, fbc:
         &&& s.scheduled_reconciles().contains_key(fbc.object_ref())
     };
     let input = fbc.object_ref();
-    FBCCluster::lemma_pre_leads_to_post_by_schedule_controller_reconcile_borrow_from_spec(spec, input, FBCCluster::next(), desired_state_is(fbc), pre, post);
-    valid_implies_implies_leads_to(spec, lift_state(post), lift_state(post));
-    or_leads_to_combine_temp(spec, lift_state(pre), lift_state(post), lift_state(post));
+    let stronger_pre = |s| {
+        &&& pre(s)
+        &&& desired_state_is(fbc)(s)
+    };
+    let stronger_next = |s, s_prime| {
+        &&& FBCCluster::next()(s, s_prime)
+        &&& desired_state_is(fbc)(s_prime)
+    };
+    always_to_always_later(spec, lift_state(desired_state_is(fbc)));
+    combine_spec_entails_always_n!(
+        spec, lift_action(stronger_next),
+        lift_action(FBCCluster::next()),
+        later(lift_state(desired_state_is(fbc)))
+    );
+    FBCCluster::lemma_pre_leads_to_post_by_schedule_controller_reconcile(spec, input, stronger_next, stronger_pre, post);
+    temp_pred_equality(lift_state(pre).and(lift_state(desired_state_is(fbc))), lift_state(stronger_pre));
+    leads_to_by_borrowing_inv(spec, lift_state(pre), lift_state(post), lift_state(desired_state_is(fbc)));
+    entails_implies_leads_to(spec, lift_state(post), lift_state(post));
+    or_leads_to_combine(spec, lift_state(pre), lift_state(post), lift_state(post));
     temp_pred_equality(lift_state(pre).or(lift_state(post)), lift_state(|s: FBCCluster| {!s.ongoing_reconciles().contains_key(fbc.object_ref())}));
 }
 
diff --git a/src/controller_examples/fluent_controller/fluentbit_config/proof/liveness/resource_match.rs b/src/controller_examples/fluent_controller/fluentbit_config/proof/liveness/resource_match.rs
index 95e443518..1c49a7f26 100644
--- a/src/controller_examples/fluent_controller/fluentbit_config/proof/liveness/resource_match.rs
+++ b/src/controller_examples/fluent_controller/fluentbit_config/proof/liveness/resource_match.rs
@@ -53,7 +53,7 @@ pub proof fn lemma_from_after_get_resource_step_to_resource_matches(spec: TempPr
         &&& s.resources().contains_key(get_request(sub_resource, fbc).key)
         &&& pending_req_in_flight_at_after_get_resource_step(sub_resource, fbc)(s)
     });
-    or_leads_to_combine_temp(spec, key_not_exists, key_exists, lift_state(sub_resource_state_matches(sub_resource, fbc)));
+    or_leads_to_combine(spec, key_not_exists, key_exists, lift_state(sub_resource_state_matches(sub_resource, fbc)));
     temp_pred_equality(
         key_not_exists.or(key_exists), lift_state(pending_req_in_flight_at_after_get_resource_step(sub_resource, fbc))
     );
@@ -153,7 +153,7 @@ pub proof fn lemma_from_after_get_resource_step_and_key_not_exists_to_resource_m
     });
 
     assert_by(spec.entails(pre.leads_to(lift_state(sub_resource_state_matches(sub_resource, fbc)))), {
-        valid_implies_implies_leads_to(spec, match_and_ok_resp, lift_state(sub_resource_state_matches(sub_resource, fbc)));
+        entails_implies_leads_to(spec, match_and_ok_resp, lift_state(sub_resource_state_matches(sub_resource, fbc)));
         leads_to_trans_n!(spec, pre, match_and_ok_resp, lift_state(sub_resource_state_matches(sub_resource, fbc)));
     });
 }
@@ -242,7 +242,7 @@ proof fn lemma_from_after_get_resource_step_and_key_exists_to_resource_matches(
     });
 
     assert_by(spec.entails(pre.leads_to(lift_state(sub_resource_state_matches(sub_resource, fbc)))), {
-        valid_implies_implies_leads_to(spec, match_and_ok_resp, lift_state(sub_resource_state_matches(sub_resource, fbc)));
+        entails_implies_leads_to(spec, match_and_ok_resp, lift_state(sub_resource_state_matches(sub_resource, fbc)));
         leads_to_trans_n!(spec, pre, match_and_ok_resp, lift_state(sub_resource_state_matches(sub_resource, fbc)));
     });
 }
@@ -712,7 +712,7 @@ pub proof fn lemma_resource_object_is_stable(
         }
     }
 
-    leads_to_stable_temp(spec, lift_action(stronger_next), p, lift_state(post));
+    leads_to_stable(spec, lift_action(stronger_next), p, lift_state(post));
 }
 
 }
diff --git a/src/controller_examples/fluent_controller/fluentbit_config/proof/liveness/terminate.rs b/src/controller_examples/fluent_controller/fluentbit_config/proof/liveness/terminate.rs
index caa278238..75253f99a 100644
--- a/src/controller_examples/fluent_controller/fluentbit_config/proof/liveness/terminate.rs
+++ b/src/controller_examples/fluent_controller/fluentbit_config/proof/liveness/terminate.rs
@@ -55,7 +55,7 @@ pub proof fn reconcile_eventually_terminates(spec: TempPred<FBCCluster>, fbc: Fl
     FBCCluster::lemma_reconcile_done_leads_to_reconcile_idle(spec, fbc.object_ref());
     temp_pred_equality(lift_state(at_step_state_pred(fbc, FluentBitConfigReconcileStep::Done)), lift_state(FBCCluster::reconciler_reconcile_done(fbc.object_ref())));
     temp_pred_equality(lift_state(at_step_state_pred(fbc, FluentBitConfigReconcileStep::Error)), lift_state(FBCCluster::reconciler_reconcile_error(fbc.object_ref())));
-    valid_implies_implies_leads_to(spec, lift_state(reconcile_idle), lift_state(reconcile_idle));
+    entails_implies_leads_to(spec, lift_state(reconcile_idle), lift_state(reconcile_idle));
 
     // Second, prove that the sub resource that every intermediate steps can lead to reconcile idle.
     lemma_from_after_get_resource_step_to_after_get_next_resource_step_to_reconcile_idle(spec, fbc, SubResource::Secret, FluentBitConfigReconcileStep::Done);
diff --git a/src/controller_examples/rabbitmq_controller/proof/helper_invariants/proof.rs b/src/controller_examples/rabbitmq_controller/proof/helper_invariants/proof.rs
index e49947ef7..4ccc3d67f 100644
--- a/src/controller_examples/rabbitmq_controller/proof/helper_invariants/proof.rs
+++ b/src/controller_examples/rabbitmq_controller/proof/helper_invariants/proof.rs
@@ -144,7 +144,7 @@ proof fn lemma_eventually_always_cm_rv_is_the_same_as_etcd_server_cm_if_cm_updat
         &&& object_in_response_at_after_update_resource_step_is_same_as_etcd(SubResource::ServerConfigMap, rabbitmq)(s)
         &&& object_in_every_resource_update_request_only_has_owner_references_pointing_to_current_cr(SubResource::ServerConfigMap, rabbitmq)(s)
     };
-    always_weaken_temp(spec, lift_state(RMQCluster::each_object_in_etcd_is_well_formed()), lift_state(resource_well_formed));
+    always_weaken(spec, lift_state(RMQCluster::each_object_in_etcd_is_well_formed()), lift_state(resource_well_formed));
     always_to_always_later(spec, lift_state(resource_well_formed));
     combine_spec_entails_always_n!(
         spec, lift_action(next), lift_action(RMQCluster::next()),
@@ -155,7 +155,7 @@ proof fn lemma_eventually_always_cm_rv_is_the_same_as_etcd_server_cm_if_cm_updat
         lift_state(object_in_response_at_after_update_resource_step_is_same_as_etcd(SubResource::ServerConfigMap, rabbitmq)),
         lift_state(object_in_every_resource_update_request_only_has_owner_references_pointing_to_current_cr(SubResource::ServerConfigMap, rabbitmq))
     );
-    leads_to_weaken_temp(
+    leads_to_weaken(
         spec, true_pred(), lift_state(|s: RMQCluster| !s.ongoing_reconciles().contains_key(rabbitmq.object_ref())),
         true_pred(), lift_state(inv)
     );
@@ -183,7 +183,7 @@ proof fn lemma_eventually_always_cm_rv_is_the_same_as_etcd_server_cm_if_cm_updat
             }
         }
     }
-    leads_to_stable_temp(spec, lift_action(next), true_pred(), lift_state(inv));
+    leads_to_stable(spec, lift_action(next), true_pred(), lift_state(inv));
 }
 
 pub proof fn lemma_eventually_always_object_in_response_at_after_create_resource_step_is_same_as_etcd_forall(
@@ -257,7 +257,7 @@ proof fn lemma_eventually_always_object_in_response_at_after_create_resource_ste
         lift_state(object_in_every_resource_update_request_only_has_owner_references_pointing_to_current_cr(SubResource::ServerConfigMap, rabbitmq)),
         lift_state(resource_object_has_no_finalizers_or_timestamp_and_only_has_controller_owner_ref(SubResource::ServerConfigMap, rabbitmq))
     );
-    leads_to_weaken_temp(
+    leads_to_weaken(
         spec, true_pred(), lift_state(|s: RMQCluster| !s.ongoing_reconciles().contains_key(rabbitmq.object_ref())),
         true_pred(), lift_state(inv)
     );
@@ -295,7 +295,7 @@ proof fn lemma_eventually_always_object_in_response_at_after_create_resource_ste
             }
         }
     }
-    leads_to_stable_temp(spec, lift_action(next), true_pred(), lift_state(inv));
+    leads_to_stable(spec, lift_action(next), true_pred(), lift_state(inv));
 }
 
 #[verifier(spinoff_prover)]
@@ -440,7 +440,7 @@ proof fn lemma_eventually_always_object_in_response_at_after_update_resource_ste
         lift_state(object_in_every_resource_update_request_only_has_owner_references_pointing_to_current_cr(SubResource::ServerConfigMap, rabbitmq)),
         lift_state(resource_object_has_no_finalizers_or_timestamp_and_only_has_controller_owner_ref(SubResource::ServerConfigMap, rabbitmq))
     );
-    leads_to_weaken_temp(
+    leads_to_weaken(
         spec, true_pred(), lift_state(|s: RMQCluster| !s.ongoing_reconciles().contains_key(rabbitmq.object_ref())),
         true_pred(), lift_state(inv)
     );
@@ -476,7 +476,7 @@ proof fn lemma_eventually_always_object_in_response_at_after_update_resource_ste
             object_in_response_at_after_update_resource_step_is_same_as_etcd_helper(s, s_prime, rabbitmq);
         }
     }
-    leads_to_stable_temp(spec, lift_action(next), true_pred(), lift_state(inv));
+    leads_to_stable(spec, lift_action(next), true_pred(), lift_state(inv));
 }
 
 #[verifier(spinoff_prover)]
@@ -1555,7 +1555,7 @@ proof fn lemma_eventually_always_no_delete_resource_request_msg_in_flight(spec:
         &&& resource_object_only_has_owner_reference_pointing_to_current_cr(sub_resource, rabbitmq)(s)
         &&& resource_well_formed(s)
     };
-    always_weaken_temp(spec, lift_state(RMQCluster::each_object_in_etcd_is_well_formed()), lift_state(resource_well_formed));
+    always_weaken(spec, lift_state(RMQCluster::each_object_in_etcd_is_well_formed()), lift_state(resource_well_formed));
     assert forall |s: RMQCluster, s_prime: RMQCluster| #[trigger] stronger_next(s, s_prime) implies RMQCluster::every_new_req_msg_if_in_flight_then_satisfies(requirements)(s, s_prime) by {
         assert forall |msg: RMQMessage| (!s.in_flight().contains(msg) || requirements(msg, s)) && #[trigger] s_prime.in_flight().contains(msg)
         implies requirements(msg, s_prime) by {
@@ -1648,9 +1648,9 @@ proof fn lemma_eventually_always_resource_object_only_has_owner_reference_pointi
 {
     let key = get_request(sub_resource, rabbitmq).key;
     let eventual_owner_ref = |owner_ref: Option<Seq<OwnerReferenceView>>| {owner_ref == Some(seq![rabbitmq.controller_owner_ref()])};
-    always_weaken_temp(spec, lift_state(object_in_every_resource_update_request_only_has_owner_references_pointing_to_current_cr(sub_resource, rabbitmq)), lift_state(RMQCluster::every_update_msg_sets_owner_references_as(key, eventual_owner_ref)));
-    always_weaken_temp(spec, lift_state(every_resource_create_request_implies_at_after_create_resource_step(sub_resource, rabbitmq)), lift_state(RMQCluster::every_create_msg_sets_owner_references_as(key, eventual_owner_ref)));
-    always_weaken_temp(spec, lift_state(resource_object_has_no_finalizers_or_timestamp_and_only_has_controller_owner_ref(sub_resource, rabbitmq)), lift_state(RMQCluster::object_has_no_finalizers(key)));
+    always_weaken(spec, lift_state(object_in_every_resource_update_request_only_has_owner_references_pointing_to_current_cr(sub_resource, rabbitmq)), lift_state(RMQCluster::every_update_msg_sets_owner_references_as(key, eventual_owner_ref)));
+    always_weaken(spec, lift_state(every_resource_create_request_implies_at_after_create_resource_step(sub_resource, rabbitmq)), lift_state(RMQCluster::every_create_msg_sets_owner_references_as(key, eventual_owner_ref)));
+    always_weaken(spec, lift_state(resource_object_has_no_finalizers_or_timestamp_and_only_has_controller_owner_ref(sub_resource, rabbitmq)), lift_state(RMQCluster::object_has_no_finalizers(key)));
 
     let state = |s: RMQCluster| {
         RMQCluster::desired_state_is(rabbitmq)(s)
diff --git a/src/controller_examples/rabbitmq_controller/proof/helper_invariants/unchangeable.rs b/src/controller_examples/rabbitmq_controller/proof/helper_invariants/unchangeable.rs
index 3018af5f8..4c7e38fe0 100644
--- a/src/controller_examples/rabbitmq_controller/proof/helper_invariants/unchangeable.rs
+++ b/src/controller_examples/rabbitmq_controller/proof/helper_invariants/unchangeable.rs
@@ -151,7 +151,7 @@ pub proof fn lemma_always_object_in_etcd_satisfies_unchangeable(spec: TempPred<R
         object_in_every_update_request_msg_satisfies_unchangeable_induction(sub_resource, rabbitmq, s, s_prime);
     }
     init_invariant(spec, RMQCluster::init(), next, inv);
-    always_weaken_temp(spec, lift_state(inv), lift_state(object_in_etcd_satisfies_unchangeable(sub_resource, rabbitmq)));
+    always_weaken(spec, lift_state(inv), lift_state(object_in_etcd_satisfies_unchangeable(sub_resource, rabbitmq)));
 }
 
 pub proof fn object_in_etcd_satisfies_unchangeable_induction(sub_resource: SubResource, rabbitmq: RabbitmqClusterView, s: RMQCluster, s_prime: RMQCluster)
diff --git a/src/controller_examples/rabbitmq_controller/proof/helper_invariants/validation.rs b/src/controller_examples/rabbitmq_controller/proof/helper_invariants/validation.rs
index 2f7027943..ecb10b8e8 100644
--- a/src/controller_examples/rabbitmq_controller/proof/helper_invariants/validation.rs
+++ b/src/controller_examples/rabbitmq_controller/proof/helper_invariants/validation.rs
@@ -230,7 +230,7 @@ pub proof fn lemma_always_object_in_resource_update_request_msg_has_smaller_rv_t
     };
     RMQCluster::lemma_always_each_object_in_etcd_is_well_formed(spec);
     lemma_always_response_at_after_get_resource_step_is_resource_get_response(spec, sub_resource, rabbitmq);
-    always_weaken_temp(spec, lift_state(RMQCluster::each_object_in_etcd_is_well_formed()), lift_state(resource_well_formed));
+    always_weaken(spec, lift_state(RMQCluster::each_object_in_etcd_is_well_formed()), lift_state(resource_well_formed));
     always_to_always_later(spec, lift_state(resource_well_formed));
     RMQCluster::lemma_always_each_object_in_reconcile_has_consistent_key_and_valid_metadata(spec);
     RMQCluster::lemma_always_object_in_ok_get_response_has_smaller_rv_than_etcd(spec);
diff --git a/src/controller_examples/rabbitmq_controller/proof/liveness/proof.rs b/src/controller_examples/rabbitmq_controller/proof/liveness/proof.rs
index 0cf4fdf22..39acf2d36 100644
--- a/src/controller_examples/rabbitmq_controller/proof/liveness/proof.rs
+++ b/src/controller_examples/rabbitmq_controller/proof/liveness/proof.rs
@@ -64,7 +64,7 @@ proof fn liveness_proof(rabbitmq: RabbitmqClusterView)
     unpack_conditions_from_spec(invariants(rabbitmq), assumption, true_pred(), always(lift_state(current_state_matches::<RabbitmqMaker>(rabbitmq))));
     temp_pred_equality(true_pred().and(assumption), assumption);
 
-    valid_implies_trans(
+    entails_trans(
         cluster_spec().and(derived_invariants_since_beginning(rabbitmq)), invariants(rabbitmq),
         always(lift_state(RMQCluster::desired_state_is(rabbitmq))).leads_to(always(lift_state(current_state_matches::<RabbitmqMaker>(rabbitmq))))
     );
@@ -84,7 +84,7 @@ proof fn spec_before_phase_n_entails_true_leads_to_current_state_matches(i: nat,
     spec_of_previous_phases_entails_eventually_new_invariants(i, rabbitmq);
     unpack_conditions_from_spec(spec_before_phase_n(i, rabbitmq), invariants_since_phase_n(i, rabbitmq), true_pred(), always(lift_state(current_state_matches::<RabbitmqMaker>(rabbitmq))));
     temp_pred_equality(true_pred().and(invariants_since_phase_n(i, rabbitmq)), invariants_since_phase_n(i, rabbitmq));
-    leads_to_trans_temp(spec_before_phase_n(i, rabbitmq), true_pred(), invariants_since_phase_n(i, rabbitmq), always(lift_state(current_state_matches::<RabbitmqMaker>(rabbitmq))));
+    leads_to_trans(spec_before_phase_n(i, rabbitmq), true_pred(), invariants_since_phase_n(i, rabbitmq), always(lift_state(current_state_matches::<RabbitmqMaker>(rabbitmq))));
 }
 
 proof fn lemma_true_leads_to_always_current_state_matches(rabbitmq: RabbitmqClusterView)
@@ -178,7 +178,7 @@ proof fn lemma_true_leads_to_always_state_matches_for_all_but_stateful_set(rabbi
         always_tla_forall_apply_for_sub_resource(spec, sub_resource, rabbitmq);
         let next_resource = next_resource_after(sub_resource).get_AfterKRequestStep_1();
         lemma_from_after_get_resource_step_to_resource_matches(spec, rabbitmq, sub_resource, next_resource);
-        leads_to_trans_temp(
+        leads_to_trans(
             spec, true_pred(), lift_state(pending_req_in_flight_at_after_get_resource_step(sub_resource, rabbitmq)),
             lift_state(sub_resource_state_matches(sub_resource, rabbitmq))
         );
@@ -259,7 +259,7 @@ proof fn lemma_true_leads_to_always_state_matches_for_stateful_set(rabbitmq: Rab
         );
         // We then prove pending_req_in_flight_at_after_get_resource_step(SubResource::StatefulSet, rabbitmq) ~> sub_resource_state_matches(SubResource::StatefulSet, rabbitmq)
         lemma_from_after_get_stateful_set_step_to_stateful_set_matches(spec, rabbitmq);
-        leads_to_trans_temp(
+        leads_to_trans(
             spec, true_pred(), lift_state(pending_req_in_flight_at_after_get_resource_step(SubResource::StatefulSet, rabbitmq)),
             lift_state(sub_resource_state_matches(SubResource::StatefulSet, rabbitmq))
         );
@@ -271,13 +271,13 @@ proof fn lemma_true_leads_to_always_state_matches_for_stateful_set(rabbitmq: Rab
         unpack_conditions_from_spec(spec2, always(lift_state(helper_invariants::stateful_set_not_exists_or_matches_or_no_more_status_update(rabbitmq))), true_pred(), always(lift_state(sub_resource_state_matches(SubResource::StatefulSet, rabbitmq))));
         temp_pred_equality(always(lift_state(helper_invariants::stateful_set_not_exists_or_matches_or_no_more_status_update(rabbitmq))), true_pred().and(always(lift_state(helper_invariants::stateful_set_not_exists_or_matches_or_no_more_status_update(rabbitmq)))));
         helper_invariants::lemma_eventually_always_stateful_set_not_exists_or_matches_or_no_more_status_update(spec2, rabbitmq);
-        leads_to_trans_temp(spec2, true_pred(), always(lift_state(helper_invariants::stateful_set_not_exists_or_matches_or_no_more_status_update(rabbitmq))), always(lift_state(sub_resource_state_matches(SubResource::StatefulSet, rabbitmq))));
+        leads_to_trans(spec2, true_pred(), always(lift_state(helper_invariants::stateful_set_not_exists_or_matches_or_no_more_status_update(rabbitmq))), always(lift_state(sub_resource_state_matches(SubResource::StatefulSet, rabbitmq))));
     });
 
     assert_by(spec1.entails(true_pred().leads_to(always(lift_state(sub_resource_state_matches(SubResource::StatefulSet, rabbitmq))))), {
         unpack_conditions_from_spec(spec1, always(lift_state(sub_resource_state_matches(SubResource::ServerConfigMap, rabbitmq))), true_pred(), always(lift_state(sub_resource_state_matches(SubResource::StatefulSet, rabbitmq))));
         temp_pred_equality(always(lift_state(sub_resource_state_matches(SubResource::ServerConfigMap, rabbitmq))), true_pred().and(always(lift_state(sub_resource_state_matches(SubResource::ServerConfigMap, rabbitmq)))));
-        leads_to_trans_temp(spec1, true_pred(), always(lift_state(sub_resource_state_matches(SubResource::ServerConfigMap, rabbitmq))), always(lift_state(sub_resource_state_matches(SubResource::StatefulSet, rabbitmq))));
+        leads_to_trans(spec1, true_pred(), always(lift_state(sub_resource_state_matches(SubResource::ServerConfigMap, rabbitmq))), always(lift_state(sub_resource_state_matches(SubResource::StatefulSet, rabbitmq))));
     });
 }
 
@@ -302,9 +302,25 @@ proof fn lemma_from_reconcile_idle_to_scheduled(spec: TempPred<RMQCluster>, rabb
         &&& s.scheduled_reconciles().contains_key(rabbitmq.object_ref())
     };
     let input = rabbitmq.object_ref();
-    RMQCluster::lemma_pre_leads_to_post_by_schedule_controller_reconcile_borrow_from_spec(spec, input, RMQCluster::next(), RMQCluster::desired_state_is(rabbitmq), pre, post);
-    valid_implies_implies_leads_to(spec, lift_state(post), lift_state(post));
-    or_leads_to_combine_temp(spec, lift_state(pre), lift_state(post), lift_state(post));
+    let stronger_pre = |s| {
+        &&& pre(s)
+        &&& desired_state_is(rabbitmq)(s)
+    };
+    let stronger_next = |s, s_prime| {
+        &&& RMQCluster::next()(s, s_prime)
+        &&& desired_state_is(rabbitmq)(s_prime)
+    };
+    always_to_always_later(spec, lift_state(desired_state_is(rabbitmq)));
+    combine_spec_entails_always_n!(
+        spec, lift_action(stronger_next),
+        lift_action(RMQCluster::next()),
+        later(lift_state(desired_state_is(rabbitmq)))
+    );
+    RMQCluster::lemma_pre_leads_to_post_by_schedule_controller_reconcile(spec, input, stronger_next, stronger_pre, post);
+    temp_pred_equality(lift_state(pre).and(lift_state(desired_state_is(rabbitmq))), lift_state(stronger_pre));
+    leads_to_by_borrowing_inv(spec, lift_state(pre), lift_state(post), lift_state(desired_state_is(rabbitmq)));
+    entails_implies_leads_to(spec, lift_state(post), lift_state(post));
+    or_leads_to_combine(spec, lift_state(pre), lift_state(post), lift_state(post));
     temp_pred_equality(lift_state(pre).or(lift_state(post)), lift_state(|s: RMQCluster| {!s.ongoing_reconciles().contains_key(rabbitmq.object_ref())}));
 }
 
diff --git a/src/controller_examples/rabbitmq_controller/proof/liveness/resource_match.rs b/src/controller_examples/rabbitmq_controller/proof/liveness/resource_match.rs
index 50ab312b1..77b2629eb 100644
--- a/src/controller_examples/rabbitmq_controller/proof/liveness/resource_match.rs
+++ b/src/controller_examples/rabbitmq_controller/proof/liveness/resource_match.rs
@@ -73,12 +73,12 @@ pub proof fn lemma_from_after_get_resource_step_to_resource_matches(
         &&& s.resources().contains_key(get_request(sub_resource, rabbitmq).key)
         &&& pending_req_in_flight_at_after_get_resource_step(sub_resource, rabbitmq)(s)
     });
-    or_leads_to_combine_temp(spec, key_not_exists, key_exists, lift_state(sub_resource_state_matches(sub_resource, rabbitmq)));
+    or_leads_to_combine(spec, key_not_exists, key_exists, lift_state(sub_resource_state_matches(sub_resource, rabbitmq)));
     temp_pred_equality(
         key_not_exists.or(key_exists), lift_state(pending_req_in_flight_at_after_get_resource_step(sub_resource, rabbitmq))
     );
     if next_resource_after(sub_resource) == after_get_k_request_step(next_resource) {
-        or_leads_to_combine_temp(spec, key_not_exists, key_exists, lift_state(pending_req_in_flight_at_after_get_resource_step(next_resource, rabbitmq)));
+        or_leads_to_combine(spec, key_not_exists, key_exists, lift_state(pending_req_in_flight_at_after_get_resource_step(next_resource, rabbitmq)));
     }
 }
 
@@ -186,7 +186,7 @@ pub proof fn lemma_from_after_get_resource_step_and_key_not_exists_to_resource_m
     });
 
     assert_by(spec.entails(pre.leads_to(lift_state(sub_resource_state_matches(sub_resource, rabbitmq)))), {
-        valid_implies_implies_leads_to(spec, match_and_ok_resp, lift_state(sub_resource_state_matches(sub_resource, rabbitmq)));
+        entails_implies_leads_to(spec, match_and_ok_resp, lift_state(sub_resource_state_matches(sub_resource, rabbitmq)));
         leads_to_trans_n!(spec, pre, match_and_ok_resp, lift_state(sub_resource_state_matches(sub_resource, rabbitmq)));
     });
 
@@ -247,7 +247,7 @@ pub proof fn lemma_from_after_get_resource_step_and_key_not_exists_to_resource_m
                 }
                 temp_pred_equality(tla_exists(known_ok_resp), exists_ok_resp);
             });
-            valid_implies_implies_leads_to(spec, match_and_ok_resp, exists_ok_resp);
+            entails_implies_leads_to(spec, match_and_ok_resp, exists_ok_resp);
             leads_to_trans_n!(spec, pre, match_and_ok_resp, exists_ok_resp, lift_state(next_state));
         });
     }
@@ -349,7 +349,7 @@ proof fn lemma_from_after_get_resource_step_and_key_exists_to_resource_matches(
     });
 
     assert_by(spec.entails(pre.leads_to(lift_state(sub_resource_state_matches(sub_resource, rabbitmq)))), {
-        valid_implies_implies_leads_to(spec, match_and_ok_resp, lift_state(sub_resource_state_matches(sub_resource, rabbitmq)));
+        entails_implies_leads_to(spec, match_and_ok_resp, lift_state(sub_resource_state_matches(sub_resource, rabbitmq)));
         leads_to_trans_n!(spec, pre, match_and_ok_resp, lift_state(sub_resource_state_matches(sub_resource, rabbitmq)));
     });
 
@@ -412,7 +412,7 @@ proof fn lemma_from_after_get_resource_step_and_key_exists_to_resource_matches(
                 }
                 temp_pred_equality(tla_exists(known_ok_resp), exists_ok_resp);
             });
-            valid_implies_implies_leads_to(spec, match_and_ok_resp, exists_ok_resp);
+            entails_implies_leads_to(spec, match_and_ok_resp, exists_ok_resp);
             leads_to_trans_n!(spec, pre, match_and_ok_resp, exists_ok_resp, lift_state(next_state));
         });
     }
@@ -562,7 +562,7 @@ proof fn lemma_from_after_get_resource_step_to_after_create_resource_step(
         &&& helper_invariants::no_create_resource_request_msg_without_name_in_flight(sub_resource, rabbitmq)(s)
         &&& helper_invariants::cm_rv_is_the_same_as_etcd_server_cm_if_cm_updated(rabbitmq)(s)
     };
-    always_weaken_temp(spec, lift_state(RMQCluster::each_object_in_reconcile_has_consistent_key_and_valid_metadata()), lift_state(consistent_key));
+    always_weaken(spec, lift_state(RMQCluster::each_object_in_reconcile_has_consistent_key_and_valid_metadata()), lift_state(consistent_key));
     combine_spec_entails_always_n!(
         spec, lift_action(stronger_next),
         lift_action(RMQCluster::next()),
@@ -919,7 +919,7 @@ proof fn lemma_from_after_get_resource_step_to_after_update_resource_step(
         &&& helper_invariants::object_in_etcd_satisfies_unchangeable(sub_resource, rabbitmq)(s)
         &&& helper_invariants::resource_object_only_has_owner_reference_pointing_to_current_cr(sub_resource, rabbitmq)(s)
     };
-    always_weaken_temp(spec, lift_state(RMQCluster::each_object_in_etcd_is_well_formed()), lift_state(resource_well_formed));
+    always_weaken(spec, lift_state(RMQCluster::each_object_in_etcd_is_well_formed()), lift_state(resource_well_formed));
 
     combine_spec_entails_always_n!(
         spec, lift_action(stronger_next),
@@ -1013,7 +1013,7 @@ pub proof fn lemma_resource_object_is_stable(
         }
     }
 
-    leads_to_stable_temp(spec, lift_action(stronger_next), p, lift_state(post));
+    leads_to_stable(spec, lift_action(stronger_next), p, lift_state(post));
 }
 
 }
diff --git a/src/controller_examples/rabbitmq_controller/proof/liveness/stateful_set_match.rs b/src/controller_examples/rabbitmq_controller/proof/liveness/stateful_set_match.rs
index f7c4fe7ad..76e4835a3 100644
--- a/src/controller_examples/rabbitmq_controller/proof/liveness/stateful_set_match.rs
+++ b/src/controller_examples/rabbitmq_controller/proof/liveness/stateful_set_match.rs
@@ -67,7 +67,7 @@ pub proof fn lemma_from_after_get_stateful_set_step_to_stateful_set_matches(
         &&& s.resources().contains_key(get_request(SubResource::StatefulSet, rabbitmq).key)
         &&& pending_req_in_flight_at_after_get_resource_step(SubResource::StatefulSet, rabbitmq)(s)
     });
-    or_leads_to_combine_temp(spec, key_not_exists, key_exists, lift_state(sub_resource_state_matches(SubResource::StatefulSet, rabbitmq)));
+    or_leads_to_combine(spec, key_not_exists, key_exists, lift_state(sub_resource_state_matches(SubResource::StatefulSet, rabbitmq)));
     temp_pred_equality(
         key_not_exists.or(key_exists), lift_state(pending_req_in_flight_at_after_get_resource_step(SubResource::StatefulSet, rabbitmq))
     );
@@ -119,7 +119,7 @@ proof fn lemma_from_after_get_stateful_set_step_and_key_exists_to_stateful_set_m
     let post = lift_state(sub_resource_state_matches(SubResource::StatefulSet, rabbitmq));
 
     assert_by(spec.entails(stateful_set_matches.leads_to(post)), {
-        valid_implies_implies_leads_to(spec, stateful_set_matches, post);
+        entails_implies_leads_to(spec, stateful_set_matches, post);
     });
 
     assert_by(spec.entails(stateful_set_not_matches.leads_to(post)), {
@@ -190,7 +190,7 @@ proof fn lemma_from_after_get_stateful_set_step_and_key_exists_to_stateful_set_m
         leads_to_trans_n!(spec, stateful_set_not_matches, post1, post2, post);
     });
 
-    or_leads_to_combine_temp(spec, stateful_set_matches, stateful_set_not_matches, post);
+    or_leads_to_combine(spec, stateful_set_matches, stateful_set_not_matches, post);
     temp_pred_equality(stateful_set_matches.or(stateful_set_not_matches), pre);
 }
 
@@ -438,7 +438,7 @@ proof fn lemma_stateful_set_state_matches_at_after_update_stateful_set_step(spec
         &&& helper_invariants::resource_object_only_has_owner_reference_pointing_to_current_cr(SubResource::StatefulSet, rabbitmq)(s)
         &&& helper_invariants::stateful_set_in_etcd_satisfies_unchangeable(rabbitmq)(s)
     };
-    always_weaken_temp(spec, lift_state(RMQCluster::each_object_in_etcd_is_well_formed()), lift_state(resource_well_formed));
+    always_weaken(spec, lift_state(RMQCluster::each_object_in_etcd_is_well_formed()), lift_state(resource_well_formed));
     combine_spec_entails_always_n!(
         spec, lift_action(stronger_next),
         lift_action(RMQCluster::next()),
@@ -526,7 +526,7 @@ pub proof fn lemma_stateful_set_is_stable(spec: TempPred<RMQCluster>, rabbitmq:
         }
     }
 
-    leads_to_stable_temp(spec, lift_action(stronger_next), p, lift_state(post));
+    leads_to_stable(spec, lift_action(stronger_next), p, lift_state(post));
 }
 
 }
diff --git a/src/controller_examples/rabbitmq_controller/proof/liveness/terminate.rs b/src/controller_examples/rabbitmq_controller/proof/liveness/terminate.rs
index 32dfcb945..95bedc71c 100644
--- a/src/controller_examples/rabbitmq_controller/proof/liveness/terminate.rs
+++ b/src/controller_examples/rabbitmq_controller/proof/liveness/terminate.rs
@@ -56,7 +56,7 @@ pub proof fn reconcile_eventually_terminates(spec: TempPred<RMQCluster>, rabbitm
     RMQCluster::lemma_reconcile_done_leads_to_reconcile_idle(spec, rabbitmq.object_ref());
     temp_pred_equality(lift_state(at_step_state_pred(rabbitmq, RabbitmqReconcileStep::Done)), lift_state(RMQCluster::reconciler_reconcile_done(rabbitmq.object_ref())));
     temp_pred_equality(lift_state(at_step_state_pred(rabbitmq, RabbitmqReconcileStep::Error)), lift_state(RMQCluster::reconciler_reconcile_error(rabbitmq.object_ref())));
-    valid_implies_implies_leads_to(spec, lift_state(reconcile_idle), lift_state(reconcile_idle));
+    entails_implies_leads_to(spec, lift_state(reconcile_idle), lift_state(reconcile_idle));
 
     // Second, prove that the sub resource that every intermediate steps can lead to reconcile idle.
     lemma_from_after_get_resource_step_to_after_get_next_resource_step_to_reconcile_idle(spec, rabbitmq, SubResource::StatefulSet, RabbitmqReconcileStep::Done);
diff --git a/src/controller_examples/v_replica_set_controller/proof/liveness/proof.rs b/src/controller_examples/v_replica_set_controller/proof/liveness/proof.rs
index 5bfdeaecb..21f27a5cb 100644
--- a/src/controller_examples/v_replica_set_controller/proof/liveness/proof.rs
+++ b/src/controller_examples/v_replica_set_controller/proof/liveness/proof.rs
@@ -13,20 +13,16 @@ use crate::kubernetes_cluster::spec::{
     message::*,
 };
 use crate::temporal_logic::{defs::*, rules::*};
-use crate::vstd_ext::{map_lib::*, string_view::*};
 use crate::v_replica_set_controller::{
-    model::{reconciler::*},
+    model::reconciler::*,
     proof::{
         helper_invariants,
-        liveness::{
-            spec::*,
-            resource_match::*,
-            terminate,
-        },
+        liveness::{resource_match::*, spec::*, terminate},
         predicate::*,
     },
     trusted::{liveness_theorem::*, spec_types::*, step::*},
 };
+use crate::vstd_ext::{map_lib::*, string_view::*};
 use vstd::{prelude::*, string::*};
 
 verus! {
@@ -34,7 +30,7 @@ verus! {
 // We prove init /\ []next /\ []wf |= []VReplicaSet::desired_state_is(vrs) ~> []current_state_matches(vrs) holds for each vrs.
 proof fn liveness_proof_forall_vrs()
    ensures liveness_theorem(),
-{	
+{
     assert forall |vrs: VReplicaSetView| #[trigger] cluster_spec().entails(liveness(vrs)) by {
         liveness_proof(vrs);
     };
@@ -59,7 +55,7 @@ proof fn liveness_proof(vrs: VReplicaSetView)
     unpack_conditions_from_spec(invariants(vrs), assumption, true_pred(), always(lift_state(current_state_matches(vrs))));
     temp_pred_equality(true_pred().and(assumption), assumption);
 
-    valid_implies_trans(
+    entails_trans(
         cluster_spec().and(derived_invariants_since_beginning(vrs)), invariants(vrs),
         always(lift_state(VRSCluster::desired_state_is(vrs))).leads_to(always(lift_state(current_state_matches(vrs))))
     );
@@ -94,7 +90,7 @@ proof fn lemma_true_leads_to_always_current_state_matches(vrs: VReplicaSetView)
             &&& num_diff_pods_is(vrs, diff)(s)
         }
     );
-        
+
     // The use of termination property ensures spec |= true ~> reconcile_idle.
     terminate::reconcile_eventually_terminates(spec, vrs);
     // Then we can continue to show that spec |= reconcile_idle ~> []current_state_matches(vrs).
@@ -113,7 +109,7 @@ proof fn lemma_true_leads_to_always_current_state_matches(vrs: VReplicaSetView)
             let diff = pods.len() - vrs.spec.replicas.unwrap_or(0);
 
             // Instantiate exists statement.
-            assert((|diff| lift_state(num_diff_pods_is(vrs, diff)))(diff).satisfied_by(ex));        
+            assert((|diff| lift_state(num_diff_pods_is(vrs, diff)))(diff).satisfied_by(ex));
         }
         assert(valid(true_pred::<VRSCluster>().implies(exists_num_diff_pods_is)));
         temp_pred_equality(true_pred::<VRSCluster>(), tla_exists(|diff| lift_state(num_diff_pods_is(vrs, diff))));
@@ -127,7 +123,7 @@ proof fn lemma_true_leads_to_always_current_state_matches(vrs: VReplicaSetView)
             let diff = choose |diff| lift_state(#[trigger] num_diff_pods_is(vrs, diff)).satisfied_by(ex);
             assert(diff_at_init(diff).satisfied_by(ex));
         }
-        implies_to_leads_to(spec, at_init, tla_exists(diff_at_init));
+        always_implies_to_leads_to(spec, at_init, tla_exists(diff_at_init));
     });
 
     // The following shows exists |diff| (num_diff_pods_is(diff) /\ init) ~> current_state_matches(vrs)
@@ -172,9 +168,25 @@ proof fn lemma_from_reconcile_idle_to_scheduled(spec: TempPred<VRSCluster>, vrs:
         &&& s.scheduled_reconciles().contains_key(vrs.object_ref())
     };
     let input = vrs.object_ref();
-    VRSCluster::lemma_pre_leads_to_post_by_schedule_controller_reconcile_borrow_from_spec(spec, input, VRSCluster::next(), VRSCluster::desired_state_is(vrs), pre, post);
-    valid_implies_implies_leads_to(spec, lift_state(post), lift_state(post));
-    or_leads_to_combine_temp(spec, lift_state(pre), lift_state(post), lift_state(post));
+    let stronger_pre = |s| {
+        &&& pre(s)
+        &&& desired_state_is(vrs)(s)
+    };
+    let stronger_next = |s, s_prime| {
+        &&& VRSCluster::next()(s, s_prime)
+        &&& desired_state_is(vrs)(s_prime)
+    };
+    always_to_always_later(spec, lift_state(desired_state_is(vrs)));
+    combine_spec_entails_always_n!(
+        spec, lift_action(stronger_next),
+        lift_action(VRSCluster::next()),
+        later(lift_state(desired_state_is(vrs)))
+    );
+    VRSCluster::lemma_pre_leads_to_post_by_schedule_controller_reconcile(spec, input, stronger_next, stronger_pre, post);
+    temp_pred_equality(lift_state(pre).and(lift_state(desired_state_is(vrs))), lift_state(stronger_pre));
+    leads_to_by_borrowing_inv(spec, lift_state(pre), lift_state(post), lift_state(desired_state_is(vrs)));
+    entails_implies_leads_to(spec, lift_state(post), lift_state(post));
+    or_leads_to_combine(spec, lift_state(pre), lift_state(post), lift_state(post));
     temp_pred_equality(lift_state(pre).or(lift_state(post)), lift_state(|s: VRSCluster| {!s.ongoing_reconciles().contains_key(vrs.object_ref())}));
 }
 
diff --git a/src/controller_examples/v_replica_set_controller/proof/liveness/resource_match.rs b/src/controller_examples/v_replica_set_controller/proof/liveness/resource_match.rs
index 4c3af685d..b369e4ed5 100644
--- a/src/controller_examples/v_replica_set_controller/proof/liveness/resource_match.rs
+++ b/src/controller_examples/v_replica_set_controller/proof/liveness/resource_match.rs
@@ -14,16 +14,13 @@ use crate::kubernetes_cluster::spec::{
     message::*,
 };
 use crate::temporal_logic::{defs::*, rules::*};
-use crate::vstd_ext::{map_lib::*, seq_lib::*, set_lib::*, string_view::*};
 use crate::v_replica_set_controller::{
-    model::{reconciler::*},
-    proof::{helper_invariants, predicate::*, liveness::api_actions::*},
-    trusted::{spec_types::*, step::*, liveness_theorem::*},
-};
-use vstd::{
-    prelude::*, seq::*, seq_lib::*, set_lib::*,
-    string::*, map::*, map_lib::*, math::abs
+    model::reconciler::*,
+    proof::{helper_invariants, liveness::api_actions::*, predicate::*},
+    trusted::{liveness_theorem::*, spec_types::*, step::*},
 };
+use crate::vstd_ext::{map_lib::*, seq_lib::*, set_lib::*, string_view::*};
+use vstd::{map::*, map_lib::*, math::abs, prelude::*, seq::*, seq_lib::*, set_lib::*, string::*};
 
 verus! {
 
@@ -107,24 +104,24 @@ pub proof fn lemma_from_diff_and_init_to_current_state_matches(
     // Deal with transition from init to listing the pods.
     lemma_from_init_step_to_send_list_pods_req(spec, vrs, diff);
 
-    assert forall |req_msg: VRSMessage| 
+    assert forall |req_msg: VRSMessage|
                  invariants implies #[trigger] spec.entails(list_req_msg(req_msg, diff).leads_to(list_resp(diff))) by {
         lemma_from_after_send_list_pods_req_to_receive_list_pods_resp(spec, vrs, req_msg, diff);
     };
     leads_to_exists_intro(spec, |req_msg| list_req_msg(req_msg, diff), list_resp(diff));
 
-    
+
     assert_by(spec.entails(list_req(diff).leads_to(tla_exists(|req_msg| list_req_msg(req_msg, diff)))), {
-        assert forall |ex| #[trigger] list_req(diff).satisfied_by(ex) 
+        assert forall |ex| #[trigger] list_req(diff).satisfied_by(ex)
             implies tla_exists(|req_msg| list_req_msg(req_msg, diff)).satisfied_by(ex) by {
             let req_msg = ex.head().ongoing_reconciles()[vrs.object_ref()].pending_req_msg.get_Some_0();
             assert((|req_msg: VRSMessage| list_req_msg(req_msg, diff))(req_msg).satisfied_by(ex));
         };
-        valid_implies_implies_leads_to(spec, list_req(diff), tla_exists(|req_msg| list_req_msg(req_msg, diff)));
+        entails_implies_leads_to(spec, list_req(diff), tla_exists(|req_msg| list_req_msg(req_msg, diff)));
     });
 
     leads_to_trans_n!(
-        spec, 
+        spec,
         pre(diff),
         list_req(diff),
         tla_exists(|req_msg| list_req_msg(req_msg, diff)),
@@ -152,10 +149,10 @@ pub proof fn lemma_from_diff_and_init_to_current_state_matches(
         // Is this enough?
         if diff + 1 == 0 {
             // If so, pre(diff) ~> current_state_matches(vrs) trivially.
-            valid_implies_implies_leads_to(spec, create_resp(diff + 1), lift_state(current_state_matches(vrs)));
+            entails_implies_leads_to(spec, create_resp(diff + 1), lift_state(current_state_matches(vrs)));
             leads_to_trans_n!(
-                spec, 
-                pre(diff), 
+                spec,
+                pre(diff),
                 create_resp(diff + 1),
                 lift_state(current_state_matches(vrs))
             );
@@ -169,16 +166,16 @@ pub proof fn lemma_from_diff_and_init_to_current_state_matches(
         // Useful assertions to let us chain in and out of ranking_pred
         assert forall |n: nat| #![trigger create_resp(-n)]
                     spec.entails(create_resp(-n).leads_to(ranking_pred(n))) by {
-            valid_implies_implies_leads_to(spec, create_resp(-n), ranking_pred(n));
+            entails_implies_leads_to(spec, create_resp(-n), ranking_pred(n));
         };
-    
+
         assert forall |n: nat| #![trigger create_resp(-n)]
                     spec.entails(ranking_pred(n).leads_to(create_resp(-n))) by {
-            valid_implies_implies_leads_to(spec, ranking_pred(n), create_resp(-n));
+            entails_implies_leads_to(spec, ranking_pred(n), create_resp(-n));
         };
 
          // Proving n > 0 => ranking_pred(n) ~> ranking_pred(n - 1)
-        assert forall |n: nat| #![trigger ranking_pred(n)] 
+        assert forall |n: nat| #![trigger ranking_pred(n)]
                     n > 0 implies spec.entails(ranking_pred(n).leads_to(ranking_pred((n - 1) as nat))) by {
             let diff = -n;
             lemma_from_after_receive_create_pod_resp_to_receive_create_pod_resp(spec, vrs, diff);
@@ -191,15 +188,15 @@ pub proof fn lemma_from_diff_and_init_to_current_state_matches(
                 ranking_pred((n - 1) as nat)
             );
         };
-        
+
         // Apply ranking function lemma
         leads_to_rank_step_one(spec, ranking_pred);
 
         // Chain everything
-        valid_implies_implies_leads_to(spec, create_resp(0), lift_state(current_state_matches(vrs)));
+        entails_implies_leads_to(spec, create_resp(0), lift_state(current_state_matches(vrs)));
         leads_to_trans_n!(
-            spec, 
-            pre(diff), 
+            spec,
+            pre(diff),
             create_resp(diff + 1),
             ranking_pred(-(diff + 1) as nat),
             ranking_pred(0),
@@ -226,10 +223,10 @@ pub proof fn lemma_from_diff_and_init_to_current_state_matches(
         // Is this enough?
         if diff - 1 == 0 {
             // If so, pre(diff) ~> current_state_matches(vrs) trivially.
-            valid_implies_implies_leads_to(spec, delete_resp(diff - 1), lift_state(current_state_matches(vrs)));
+            entails_implies_leads_to(spec, delete_resp(diff - 1), lift_state(current_state_matches(vrs)));
             leads_to_trans_n!(
-                spec, 
-                pre(diff), 
+                spec,
+                pre(diff),
                 delete_resp(diff - 1),
                 lift_state(current_state_matches(vrs))
             );
@@ -241,16 +238,16 @@ pub proof fn lemma_from_diff_and_init_to_current_state_matches(
         // Useful assertions to let us chain in and out of ranking_pred
         assert forall |n: nat| #![trigger ranking_pred(n)]
                     spec.entails(delete_resp(n as int).leads_to(ranking_pred(n))) by {
-            valid_implies_implies_leads_to(spec, delete_resp(n as int), ranking_pred(n));
+            entails_implies_leads_to(spec, delete_resp(n as int), ranking_pred(n));
         };
-    
+
         assert forall |n: nat| #![trigger ranking_pred(n)]
                     spec.entails(ranking_pred(n).leads_to(delete_resp(n as int))) by {
-            valid_implies_implies_leads_to(spec, ranking_pred(n), delete_resp(n as int));
+            entails_implies_leads_to(spec, ranking_pred(n), delete_resp(n as int));
         };
 
          // Proving n > 0 => ranking_pred(n) ~> ranking_pred(n - 1)
-        assert forall |n: nat| #![trigger ranking_pred(n)] 
+        assert forall |n: nat| #![trigger ranking_pred(n)]
                     n > 0 implies spec.entails(ranking_pred(n).leads_to(ranking_pred((n - 1) as nat))) by {
             let diff = n as int;
             lemma_from_after_receive_delete_pod_resp_to_receive_delete_pod_resp(spec, vrs, diff);
@@ -263,15 +260,15 @@ pub proof fn lemma_from_diff_and_init_to_current_state_matches(
                 ranking_pred((n - 1) as nat)
             );
         };
-        
+
         // Apply ranking function lemma
         leads_to_rank_step_one(spec, ranking_pred);
 
         // Chain everything
-        valid_implies_implies_leads_to(spec, delete_resp(0), lift_state(current_state_matches(vrs)));
+        entails_implies_leads_to(spec, delete_resp(0), lift_state(current_state_matches(vrs)));
         leads_to_trans_n!(
-            spec, 
-            pre(diff), 
+            spec,
+            pre(diff),
             delete_resp(diff - 1),
             ranking_pred((diff - 1) as nat),
             ranking_pred(0),
@@ -281,9 +278,9 @@ pub proof fn lemma_from_diff_and_init_to_current_state_matches(
     } else {
         // diff = 0
         // list_resp(diff) ~> current_state_matches(vrs) trivially.
-        valid_implies_implies_leads_to(spec, list_resp(diff), lift_state(current_state_matches(vrs)));
+        entails_implies_leads_to(spec, list_resp(diff), lift_state(current_state_matches(vrs)));
         leads_to_trans_n!(
-            spec, 
+            spec,
             pre(diff),
             list_resp(diff),
             lift_state(current_state_matches(vrs))
@@ -458,7 +455,7 @@ pub proof fn lemma_from_after_send_list_pods_req_to_receive_list_pods_resp(
                     let resp_msg = VRSCluster::handle_list_request_msg(req_msg, s.kubernetes_api_state).1;
                     let resp_objs = resp_msg.content.get_list_response().res.unwrap();
 
-                    assert forall |o: DynamicObjectView| #![auto] 
+                    assert forall |o: DynamicObjectView| #![auto]
                     pre(s) && matching_pod_entries(vrs, s_prime.resources()).values().contains(o)
                     implies resp_objs.to_set().contains(o) by {
                         // Tricky reasoning about .to_seq
@@ -472,7 +469,7 @@ pub proof fn lemma_from_after_send_list_pods_req_to_receive_list_pods_resp(
                         finite_set_to_seq_contains_all_set_elements(selected_elements);
                     }
 
-                    assert forall |o: DynamicObjectView| #![auto] 
+                    assert forall |o: DynamicObjectView| #![auto]
                     pre(s) && resp_objs.contains(o)
                     implies !PodView::unmarshal(o).is_err() by {
                         // Tricky reasoning about .to_seq
@@ -510,7 +507,7 @@ pub proof fn lemma_from_after_send_list_pods_req_to_receive_list_pods_resp(
         let resp_msg = VRSCluster::handle_list_request_msg(req_msg, s.kubernetes_api_state).1;
         let resp_objs = resp_msg.content.get_list_response().res.unwrap();
 
-        assert forall |o: DynamicObjectView| #![auto] 
+        assert forall |o: DynamicObjectView| #![auto]
         pre(s) && matching_pod_entries(vrs, s_prime.resources()).values().contains(o)
         implies resp_objs.to_set().contains(o) by {
             // Tricky reasoning about .to_seq
@@ -524,7 +521,7 @@ pub proof fn lemma_from_after_send_list_pods_req_to_receive_list_pods_resp(
             finite_set_to_seq_contains_all_set_elements(selected_elements);
         }
 
-        assert forall |o: DynamicObjectView| #![auto] 
+        assert forall |o: DynamicObjectView| #![auto]
         pre(s) && resp_objs.contains(o)
         implies !PodView::unmarshal(o).is_err() by {
             // Tricky reasoning about .to_seq
@@ -563,7 +560,7 @@ pub proof fn lemma_from_after_send_list_pods_req_to_receive_list_pods_resp(
 pub proof fn lemma_from_after_receive_list_pods_resp_to_receive_create_pod_resp(
     spec: TempPred<VRSCluster>, vrs: VReplicaSetView, diff: int
 )
-    requires 
+    requires
         spec.entails(always(lift_action(VRSCluster::next()))),
         spec.entails(tla_forall(|i| VRSCluster::controller_next().weak_fairness(i))),
         spec.entails(tla_forall(|i| VRSCluster::kubernetes_api_next().weak_fairness(i))),
@@ -636,11 +633,11 @@ pub proof fn lemma_from_after_receive_list_pods_resp_to_receive_create_pod_resp(
     );
 
     // Apply two lemmas relating to the first created pod.
-    assert forall |resp_msg: VRSMessage| 
+    assert forall |resp_msg: VRSMessage|
                 diff < 0 implies #[trigger] spec.entails(list_resp_msg(resp_msg, diff).leads_to(create_req(diff))) by {
         lemma_from_after_receive_list_pods_resp_to_send_create_pod_req(spec, vrs, resp_msg, diff);
     };
-    assert forall |req_msg: VRSMessage| 
+    assert forall |req_msg: VRSMessage|
                 diff < 0 implies #[trigger] spec.entails(create_req_msg(req_msg, diff).leads_to(create_resp(diff + 1))) by {
         lemma_from_after_send_create_pod_req_to_receive_ok_resp(spec, vrs, req_msg, diff);
     };
@@ -651,7 +648,7 @@ pub proof fn lemma_from_after_receive_list_pods_resp_to_receive_create_pod_resp(
     assert_by(
         spec.entails(list_resp(diff).leads_to(tla_exists(|resp_msg: VRSMessage| list_resp_msg(resp_msg, diff)))),
         {
-            assert forall |ex| #[trigger] list_resp(diff).satisfied_by(ex) 
+            assert forall |ex| #[trigger] list_resp(diff).satisfied_by(ex)
                 implies tla_exists(|resp_msg: VRSMessage| list_resp_msg(resp_msg, diff)).satisfied_by(ex) by {
                 let s = ex.head();
                 let msg = s.ongoing_reconciles()[vrs.object_ref()].pending_req_msg.get_Some_0();
@@ -668,24 +665,24 @@ pub proof fn lemma_from_after_receive_list_pods_resp_to_receive_create_pod_resp(
                 };
                 assert((|resp_msg: VRSMessage| list_resp_msg(resp_msg, diff))(resp_msg).satisfied_by(ex));
             };
-            valid_implies_implies_leads_to(spec, list_resp(diff), tla_exists(|resp_msg: VRSMessage| list_resp_msg(resp_msg, diff)));
+            entails_implies_leads_to(spec, list_resp(diff), tla_exists(|resp_msg: VRSMessage| list_resp_msg(resp_msg, diff)));
         }
     );
     assert_by(
         spec.entails(create_req(diff).leads_to(tla_exists(|req_msg: VRSMessage| create_req_msg(req_msg, diff)))),
         {
-            assert forall |ex| #[trigger] create_req(diff).satisfied_by(ex) 
+            assert forall |ex| #[trigger] create_req(diff).satisfied_by(ex)
                 implies tla_exists(|req_msg: VRSMessage| create_req_msg(req_msg, diff)).satisfied_by(ex) by {
                 let req_msg = ex.head().ongoing_reconciles()[vrs.object_ref()].pending_req_msg.get_Some_0();
                 assert((|req_msg: VRSMessage| create_req_msg(req_msg, diff))(req_msg).satisfied_by(ex));
             };
-            valid_implies_implies_leads_to(spec, create_req(diff), tla_exists(|req_msg: VRSMessage| create_req_msg(req_msg, diff)));
+            entails_implies_leads_to(spec, create_req(diff), tla_exists(|req_msg: VRSMessage| create_req_msg(req_msg, diff)));
         }
     );
     leads_to_trans_n!(
         spec,
         list_resp(diff),
-        tla_exists(|resp_msg: VRSMessage| list_resp_msg(resp_msg, diff)), 
+        tla_exists(|resp_msg: VRSMessage| list_resp_msg(resp_msg, diff)),
         create_req(diff),
         tla_exists(|req_msg: VRSMessage| create_req_msg(req_msg, diff)),
         create_resp(diff + 1)
@@ -754,11 +751,11 @@ pub proof fn lemma_from_after_receive_create_pod_resp_to_receive_create_pod_resp
     );
 
     // Apply two lemmas relating to subsequent created pods.
-    assert forall |resp_msg: VRSMessage| 
+    assert forall |resp_msg: VRSMessage|
                 diff < 0 implies #[trigger] spec.entails(create_resp_msg(resp_msg, diff).leads_to(create_req(diff))) by {
         lemma_from_after_receive_ok_resp_to_send_create_pod_req(spec, vrs, resp_msg, diff);
     };
-    assert forall |req_msg: VRSMessage| 
+    assert forall |req_msg: VRSMessage|
                 diff < 0 implies #[trigger] spec.entails(create_req_msg(req_msg, diff).leads_to(create_resp(diff + 1))) by {
         lemma_from_after_send_create_pod_req_to_receive_ok_resp(spec, vrs, req_msg, diff);
     };
@@ -769,18 +766,18 @@ pub proof fn lemma_from_after_receive_create_pod_resp_to_receive_create_pod_resp
     assert_by(
         spec.entails(create_req(diff).leads_to(tla_exists(|req_msg: VRSMessage| create_req_msg(req_msg, diff)))),
         {
-            assert forall |ex| #[trigger] create_req(diff).satisfied_by(ex) 
+            assert forall |ex| #[trigger] create_req(diff).satisfied_by(ex)
                 implies tla_exists(|req_msg: VRSMessage| create_req_msg(req_msg, diff)).satisfied_by(ex) by {
                 let req_msg = ex.head().ongoing_reconciles()[vrs.object_ref()].pending_req_msg.get_Some_0();
                 assert((|req_msg: VRSMessage| create_req_msg(req_msg, diff))(req_msg).satisfied_by(ex));
             };
-            valid_implies_implies_leads_to(spec, create_req(diff), tla_exists(|req_msg: VRSMessage| create_req_msg(req_msg, diff)));
+            entails_implies_leads_to(spec, create_req(diff), tla_exists(|req_msg: VRSMessage| create_req_msg(req_msg, diff)));
         }
     );
     assert_by(
         spec.entails(create_resp(diff).leads_to(tla_exists(|resp_msg: VRSMessage| create_resp_msg(resp_msg, diff)))),
         {
-            assert forall |ex| #[trigger] create_resp(diff).satisfied_by(ex) 
+            assert forall |ex| #[trigger] create_resp(diff).satisfied_by(ex)
                 implies tla_exists(|resp_msg: VRSMessage| create_resp_msg(resp_msg, diff)).satisfied_by(ex) by {
                 let s = ex.head();
                 let msg = s.ongoing_reconciles()[vrs.object_ref()].pending_req_msg.get_Some_0();
@@ -791,7 +788,7 @@ pub proof fn lemma_from_after_receive_create_pod_resp_to_receive_create_pod_resp
                 };
                 assert((|resp_msg: VRSMessage| create_resp_msg(resp_msg, diff))(resp_msg).satisfied_by(ex));
             };
-            valid_implies_implies_leads_to(spec, create_resp(diff), tla_exists(|resp_msg: VRSMessage| create_resp_msg(resp_msg, diff)));
+            entails_implies_leads_to(spec, create_resp(diff), tla_exists(|resp_msg: VRSMessage| create_resp_msg(resp_msg, diff)));
         }
     );
 
@@ -932,7 +929,7 @@ pub proof fn lemma_filtered_pods_len_equals_matching_pods_len(
 pub proof fn lemma_from_after_send_create_pod_req_to_receive_ok_resp(
     spec: TempPred<VRSCluster>, vrs: VReplicaSetView, req_msg: VRSMessage, diff: int
 )
-    requires 
+    requires
         spec.entails(always(lift_action(VRSCluster::next()))),
         spec.entails(tla_forall(|i| VRSCluster::kubernetes_api_next().weak_fairness(i))),
         spec.entails(always(lift_state(VRSCluster::crash_disabled()))),
@@ -1109,7 +1106,7 @@ pub proof fn lemma_from_after_send_create_pod_req_to_receive_ok_resp(
 pub proof fn lemma_from_after_receive_ok_resp_to_send_create_pod_req(
     spec: TempPred<VRSCluster>, vrs: VReplicaSetView, resp_msg: VRSMessage, diff: int
 )
-    requires 
+    requires
         spec.entails(always(lift_action(VRSCluster::next()))),
         spec.entails(tla_forall(|i| VRSCluster::controller_next().weak_fairness(i))),
         spec.entails(always(lift_state(VRSCluster::crash_disabled()))),
@@ -1205,7 +1202,7 @@ pub proof fn lemma_from_after_receive_ok_resp_to_send_create_pod_req(
 pub proof fn lemma_from_after_receive_list_pods_resp_to_receive_delete_pod_resp(
     spec: TempPred<VRSCluster>, vrs: VReplicaSetView, diff: int
 )
-    requires 
+    requires
         spec.entails(always(lift_action(VRSCluster::next()))),
         spec.entails(tla_forall(|i| VRSCluster::controller_next().weak_fairness(i))),
         spec.entails(tla_forall(|i| VRSCluster::kubernetes_api_next().weak_fairness(i))),
@@ -1278,11 +1275,11 @@ pub proof fn lemma_from_after_receive_list_pods_resp_to_receive_delete_pod_resp(
     );
 
     // Apply two lemmas relating to the first deleted pod.
-    assert forall |resp_msg: VRSMessage| 
+    assert forall |resp_msg: VRSMessage|
                 diff > 0 implies #[trigger] spec.entails(list_resp_msg(resp_msg, diff).leads_to(delete_req(diff))) by {
         lemma_from_after_receive_list_pods_resp_to_send_delete_pod_req(spec, vrs, resp_msg, diff);
     };
-    assert forall |req_msg: VRSMessage| 
+    assert forall |req_msg: VRSMessage|
                 diff > 0 implies #[trigger] spec.entails(delete_req_msg(req_msg, diff).leads_to(delete_resp(diff - 1))) by {
         lemma_from_after_send_delete_pod_req_to_receive_ok_resp(spec, vrs, req_msg, diff);
     };
@@ -1293,7 +1290,7 @@ pub proof fn lemma_from_after_receive_list_pods_resp_to_receive_delete_pod_resp(
     assert_by(
         spec.entails(list_resp(diff).leads_to(tla_exists(|resp_msg: VRSMessage| list_resp_msg(resp_msg, diff)))),
         {
-            assert forall |ex| #[trigger] list_resp(diff).satisfied_by(ex) 
+            assert forall |ex| #[trigger] list_resp(diff).satisfied_by(ex)
                 implies tla_exists(|resp_msg: VRSMessage| list_resp_msg(resp_msg, diff)).satisfied_by(ex) by {
                 let s = ex.head();
                 let msg = s.ongoing_reconciles()[vrs.object_ref()].pending_req_msg.get_Some_0();
@@ -1310,24 +1307,24 @@ pub proof fn lemma_from_after_receive_list_pods_resp_to_receive_delete_pod_resp(
                 };
                 assert((|resp_msg: VRSMessage| list_resp_msg(resp_msg, diff))(resp_msg).satisfied_by(ex));
             };
-            valid_implies_implies_leads_to(spec, list_resp(diff), tla_exists(|resp_msg: VRSMessage| list_resp_msg(resp_msg, diff)));
+            entails_implies_leads_to(spec, list_resp(diff), tla_exists(|resp_msg: VRSMessage| list_resp_msg(resp_msg, diff)));
         }
     );
     assert_by(
         spec.entails(delete_req(diff).leads_to(tla_exists(|req_msg: VRSMessage| delete_req_msg(req_msg, diff)))),
         {
-            assert forall |ex| #[trigger] delete_req(diff).satisfied_by(ex) 
+            assert forall |ex| #[trigger] delete_req(diff).satisfied_by(ex)
                 implies tla_exists(|req_msg: VRSMessage| delete_req_msg(req_msg, diff)).satisfied_by(ex) by {
                 let req_msg = ex.head().ongoing_reconciles()[vrs.object_ref()].pending_req_msg.get_Some_0();
                 assert((|req_msg: VRSMessage| delete_req_msg(req_msg, diff))(req_msg).satisfied_by(ex));
             };
-            valid_implies_implies_leads_to(spec, delete_req(diff), tla_exists(|req_msg: VRSMessage| delete_req_msg(req_msg, diff)));
+            entails_implies_leads_to(spec, delete_req(diff), tla_exists(|req_msg: VRSMessage| delete_req_msg(req_msg, diff)));
         }
     );
     leads_to_trans_n!(
         spec,
         list_resp(diff),
-        tla_exists(|resp_msg: VRSMessage| list_resp_msg(resp_msg, diff)), 
+        tla_exists(|resp_msg: VRSMessage| list_resp_msg(resp_msg, diff)),
         delete_req(diff),
         tla_exists(|req_msg: VRSMessage| delete_req_msg(req_msg, diff)),
         delete_resp(diff - 1)
@@ -1398,11 +1395,11 @@ pub proof fn lemma_from_after_receive_delete_pod_resp_to_receive_delete_pod_resp
     );
 
     // Apply two lemmas relating to subsequent deleted pods.
-    assert forall |resp_msg: VRSMessage| 
+    assert forall |resp_msg: VRSMessage|
                 diff > 0 implies #[trigger] spec.entails(delete_resp_msg(resp_msg, diff).leads_to(delete_req(diff))) by {
         lemma_from_after_receive_ok_resp_to_send_delete_pod_req(spec, vrs, resp_msg, diff);
     };
-    assert forall |req_msg: VRSMessage| 
+    assert forall |req_msg: VRSMessage|
                 diff > 0 implies #[trigger] spec.entails(delete_req_msg(req_msg, diff).leads_to(delete_resp(diff - 1))) by {
         lemma_from_after_send_delete_pod_req_to_receive_ok_resp(spec, vrs, req_msg, diff);
     };
@@ -1413,18 +1410,18 @@ pub proof fn lemma_from_after_receive_delete_pod_resp_to_receive_delete_pod_resp
     assert_by(
         spec.entails(delete_req(diff).leads_to(tla_exists(|req_msg: VRSMessage| delete_req_msg(req_msg, diff)))),
         {
-            assert forall |ex| #[trigger] delete_req(diff).satisfied_by(ex) 
+            assert forall |ex| #[trigger] delete_req(diff).satisfied_by(ex)
                 implies tla_exists(|req_msg: VRSMessage| delete_req_msg(req_msg, diff)).satisfied_by(ex) by {
                 let req_msg = ex.head().ongoing_reconciles()[vrs.object_ref()].pending_req_msg.get_Some_0();
                 assert((|req_msg: VRSMessage| delete_req_msg(req_msg, diff))(req_msg).satisfied_by(ex));
             };
-            valid_implies_implies_leads_to(spec, delete_req(diff), tla_exists(|req_msg: VRSMessage| delete_req_msg(req_msg, diff)));
+            entails_implies_leads_to(spec, delete_req(diff), tla_exists(|req_msg: VRSMessage| delete_req_msg(req_msg, diff)));
         }
     );
     assert_by(
         spec.entails(delete_resp(diff).leads_to(tla_exists(|resp_msg: VRSMessage| delete_resp_msg(resp_msg, diff)))),
         {
-            assert forall |ex| #[trigger] delete_resp(diff).satisfied_by(ex) 
+            assert forall |ex| #[trigger] delete_resp(diff).satisfied_by(ex)
                 implies tla_exists(|resp_msg: VRSMessage| delete_resp_msg(resp_msg, diff)).satisfied_by(ex) by {
                 let s = ex.head();
                 let msg = s.ongoing_reconciles()[vrs.object_ref()].pending_req_msg.get_Some_0();
@@ -1435,7 +1432,7 @@ pub proof fn lemma_from_after_receive_delete_pod_resp_to_receive_delete_pod_resp
                 };
                 assert((|resp_msg: VRSMessage| delete_resp_msg(resp_msg, diff))(resp_msg).satisfied_by(ex));
             };
-            valid_implies_implies_leads_to(spec, delete_resp(diff), tla_exists(|resp_msg: VRSMessage| delete_resp_msg(resp_msg, diff)));
+            entails_implies_leads_to(spec, delete_resp(diff), tla_exists(|resp_msg: VRSMessage| delete_resp_msg(resp_msg, diff)));
         }
     );
 
@@ -1452,7 +1449,7 @@ pub proof fn lemma_from_after_receive_delete_pod_resp_to_receive_delete_pod_resp
 pub proof fn lemma_from_after_receive_list_pods_resp_to_send_delete_pod_req(
     spec: TempPred<VRSCluster>, vrs: VReplicaSetView, resp_msg: VRSMessage, diff: int
 )
-    requires 
+    requires
         spec.entails(always(lift_action(VRSCluster::next()))),
         spec.entails(tla_forall(|i| VRSCluster::controller_next().weak_fairness(i))),
         spec.entails(always(lift_state(VRSCluster::crash_disabled()))),
@@ -1581,7 +1578,7 @@ pub proof fn lemma_filtered_pods_set_equals_matching_pods(
 // filter_pods filters pods in a very similar way to matching_pods, but the former
 // works on a sequence of PodViews, while the latter works on the key-value store directly.
 // I need to do some manual effort to make the two representations work together.
-// 
+//
 // Once proven, this will supplant the earlier lemma
 // lemma_filtered_pods_len_equals_matching_pods_len.
 //
@@ -1716,7 +1713,7 @@ pub proof fn lemma_from_after_send_delete_pod_req_to_receive_ok_resp(
 pub proof fn lemma_from_after_receive_ok_resp_to_send_delete_pod_req(
     spec: TempPred<VRSCluster>, vrs: VReplicaSetView, resp_msg: VRSMessage, diff: int
 )
-    requires 
+    requires
         spec.entails(always(lift_action(VRSCluster::next()))),
         spec.entails(tla_forall(|i| VRSCluster::controller_next().weak_fairness(i))),
         spec.entails(always(lift_state(VRSCluster::crash_disabled()))),
@@ -1863,7 +1860,7 @@ pub proof fn lemma_current_state_matches_is_stable(
         }
     }
 
-    leads_to_stable_temp(spec, lift_action(stronger_next), p, lift_state(post));
+    leads_to_stable(spec, lift_action(stronger_next), p, lift_state(post));
 }
 //
 // TODO: Prove this.
diff --git a/src/controller_examples/v_replica_set_controller/proof/liveness/terminate.rs b/src/controller_examples/v_replica_set_controller/proof/liveness/terminate.rs
index de3debd08..d2ecc8953 100644
--- a/src/controller_examples/v_replica_set_controller/proof/liveness/terminate.rs
+++ b/src/controller_examples/v_replica_set_controller/proof/liveness/terminate.rs
@@ -41,7 +41,7 @@ pub proof fn reconcile_eventually_terminates(spec: TempPred<VRSCluster>, vrs: VR
         spec.entails(always(tla_forall(|diff: usize| lift_state(VRSCluster::pending_req_in_flight_or_resp_in_flight_at_reconcile_state(
                 vrs.object_ref(), at_step_closure(VReplicaSetReconcileStep::AfterDeletePod(diff))
             ))))),
-        
+
     ensures spec.entails(true_pred().leads_to(lift_state(|s: VRSCluster| !s.ongoing_reconciles().contains_key(vrs.object_ref())))),
 {
     assert forall |diff: usize| #![auto]
@@ -73,7 +73,7 @@ pub proof fn reconcile_eventually_terminates(spec: TempPred<VRSCluster>, vrs: VR
     VRSCluster::lemma_reconcile_done_leads_to_reconcile_idle(spec, vrs.object_ref());
     temp_pred_equality(lift_state(at_step_state_pred(vrs, VReplicaSetReconcileStep::Done)), lift_state(VRSCluster::reconciler_reconcile_done(vrs.object_ref())));
     temp_pred_equality(lift_state(at_step_state_pred(vrs, VReplicaSetReconcileStep::Error)), lift_state(VRSCluster::reconciler_reconcile_error(vrs.object_ref())));
-    valid_implies_implies_leads_to(spec, lift_state(reconcile_idle), lift_state(reconcile_idle));
+    entails_implies_leads_to(spec, lift_state(reconcile_idle), lift_state(reconcile_idle));
 
     // Second, prove that after_create_pod_rank(0) \/ after_delete_pod_rank(0) ~> reconcile_idle.
     lemma_from_after_create_or_delete_pod_rank_zero_to_reconcile_idle(spec, vrs);
@@ -89,22 +89,22 @@ pub proof fn reconcile_eventually_terminates(spec: TempPred<VRSCluster>, vrs: VR
         }
         leads_to_rank_step_one_usize(spec, |n| lift_state(after_create_pod_rank(vrs, n)));
 
-        implies_to_leads_to(
-            spec, 
+        always_implies_to_leads_to(
+            spec,
             lift_state(at_step_state_pred(vrs, VReplicaSetReconcileStep::AfterCreatePod(n))),
             lift_state(after_create_pod_rank(vrs, n))
         );
         assert(spec.entails((|n| lift_state(after_create_pod_rank(vrs, n)))(n)
                                 .leads_to((|n| lift_state(after_create_pod_rank(vrs, n)))(0))));
         leads_to_trans_n!(
-            spec, 
+            spec,
             lift_state(at_step_state_pred(vrs, VReplicaSetReconcileStep::AfterCreatePod(n))),
-            lift_state(after_create_pod_rank(vrs, n)), 
-            lift_state(after_create_pod_rank(vrs, 0)), 
+            lift_state(after_create_pod_rank(vrs, n)),
+            lift_state(after_create_pod_rank(vrs, 0)),
             lift_state(reconcile_idle)
         );
     }
-    
+
     // Similarly prove for all n that AfterDeletePod(n) ~> reconcile_idle.
     assert forall |n: usize| #![auto]
         spec.entails(lift_state(at_step_state_pred(vrs, VReplicaSetReconcileStep::AfterDeletePod(n)))
@@ -115,9 +115,9 @@ pub proof fn reconcile_eventually_terminates(spec: TempPred<VRSCluster>, vrs: VR
             lemma_from_after_delete_pod_rank_n_to_delete_pod_rank_n_minus_1(spec, vrs, n);
         }
         leads_to_rank_step_one_usize(spec, |n| lift_state(after_delete_pod_rank(vrs, n)));
-        
-        implies_to_leads_to(
-            spec, 
+
+        always_implies_to_leads_to(
+            spec,
             lift_state(at_step_state_pred(vrs, VReplicaSetReconcileStep::AfterDeletePod(n))),
             lift_state(after_delete_pod_rank(vrs, n))
         );
@@ -138,15 +138,15 @@ pub proof fn reconcile_eventually_terminates(spec: TempPred<VRSCluster>, vrs: VR
     // Fifth, prove that reconcile init state can reach AfterListPods.
     VRSCluster::lemma_from_init_state_to_next_state_to_reconcile_idle(
         spec, vrs, at_step_closure(VReplicaSetReconcileStep::Init), at_step_closure(VReplicaSetReconcileStep::AfterListPods));
-    
+
     // Finally, combine all cases
     leads_to_exists_intro(
-        spec, 
+        spec,
         |n| lift_state(at_step_state_pred(vrs, VReplicaSetReconcileStep::AfterCreatePod(n))),
         lift_state(reconcile_idle)
     );
     leads_to_exists_intro(
-        spec, 
+        spec,
         |n| lift_state(at_step_state_pred(vrs, VReplicaSetReconcileStep::AfterDeletePod(n))),
         lift_state(reconcile_idle)
     );
@@ -274,23 +274,23 @@ proof fn lemma_from_after_create_pod_rank_n_to_create_pod_rank_n_minus_1(
         || s.reconcile_step == VReplicaSetReconcileStep::Error
     };
 
-    valid_implies_implies_leads_to(
-        spec, 
-        lift_state(at_step_state_pred(vrs, VReplicaSetReconcileStep::Error)), 
+    entails_implies_leads_to(
+        spec,
+        lift_state(at_step_state_pred(vrs, VReplicaSetReconcileStep::Error)),
         lift_state(after_create_pod_rank(vrs, (n - 1) as usize))
     );
-    
+
     VRSCluster::lemma_from_some_state_to_arbitrary_next_state(spec, vrs, at_step_closure(VReplicaSetReconcileStep::AfterCreatePod(n)), state_after_create);
 
-    implies_to_leads_to(
-        spec, 
-        lift_state(VRSCluster::at_expected_reconcile_states(vrs.object_ref(), state_after_create)), 
+    always_implies_to_leads_to(
+        spec,
+        lift_state(VRSCluster::at_expected_reconcile_states(vrs.object_ref(), state_after_create)),
         lift_state(after_create_pod_rank(vrs, (n - 1) as usize))
     );
     leads_to_trans_n!(
         spec,
         lift_state(at_step_state_pred(vrs, VReplicaSetReconcileStep::AfterCreatePod(n))),
-        lift_state(VRSCluster::at_expected_reconcile_states(vrs.object_ref(), state_after_create)), 
+        lift_state(VRSCluster::at_expected_reconcile_states(vrs.object_ref(), state_after_create)),
         lift_state(after_create_pod_rank(vrs, (n - 1) as usize))
     );
 
@@ -327,23 +327,23 @@ proof fn lemma_from_after_delete_pod_rank_n_to_delete_pod_rank_n_minus_1(
         || s.reconcile_step == VReplicaSetReconcileStep::Error
     };
 
-    valid_implies_implies_leads_to(
-        spec, 
-        lift_state(at_step_state_pred(vrs, VReplicaSetReconcileStep::Error)), 
+    entails_implies_leads_to(
+        spec,
+        lift_state(at_step_state_pred(vrs, VReplicaSetReconcileStep::Error)),
         lift_state(after_delete_pod_rank(vrs, (n - 1) as usize))
     );
-    
+
     VRSCluster::lemma_from_some_state_to_arbitrary_next_state(spec, vrs, at_step_closure(VReplicaSetReconcileStep::AfterDeletePod(n)), state_after_delete);
 
-    implies_to_leads_to(
-        spec, 
-        lift_state(VRSCluster::at_expected_reconcile_states(vrs.object_ref(), state_after_delete)), 
+    always_implies_to_leads_to(
+        spec,
+        lift_state(VRSCluster::at_expected_reconcile_states(vrs.object_ref(), state_after_delete)),
         lift_state(after_delete_pod_rank(vrs, (n - 1) as usize))
     );
     leads_to_trans_n!(
         spec,
         lift_state(at_step_state_pred(vrs, VReplicaSetReconcileStep::AfterDeletePod(n))),
-        lift_state(VRSCluster::at_expected_reconcile_states(vrs.object_ref(), state_after_delete)), 
+        lift_state(VRSCluster::at_expected_reconcile_states(vrs.object_ref(), state_after_delete)),
         lift_state(after_delete_pod_rank(vrs, (n - 1) as usize))
     );
 
@@ -392,12 +392,12 @@ proof fn lemma_from_after_list_pods_to_reconcile_idle(
         ||| s.reconcile_step == VReplicaSetReconcileStep::Error
     };
     leads_to_exists_intro(
-        spec, 
+        spec,
         |n| lift_state(at_step_state_pred(vrs, VReplicaSetReconcileStep::AfterCreatePod(n))),
         lift_state(|s: VRSCluster| !s.ongoing_reconciles().contains_key(vrs.object_ref()))
     );
     leads_to_exists_intro(
-        spec, 
+        spec,
         |n| lift_state(at_step_state_pred(vrs, VReplicaSetReconcileStep::AfterDeletePod(n))),
         lift_state(|s: VRSCluster| !s.ongoing_reconciles().contains_key(vrs.object_ref()))
     );
@@ -413,9 +413,9 @@ proof fn lemma_from_after_list_pods_to_reconcile_idle(
         lift_state(VRSCluster::at_expected_reconcile_states(vrs.object_ref(), |s: VReplicaSetReconcileState|
         exists |n: usize| s.reconcile_step == VReplicaSetReconcileStep::AfterCreatePod(n))),
         {
-            assert forall |ex| #![auto] 
+            assert forall |ex| #![auto]
             lift_state(VRSCluster::at_expected_reconcile_states(vrs.object_ref(), |s: VReplicaSetReconcileState|
-            exists |n: usize| s.reconcile_step == VReplicaSetReconcileStep::AfterCreatePod(n))).satisfied_by(ex) implies 
+            exists |n: usize| s.reconcile_step == VReplicaSetReconcileStep::AfterCreatePod(n))).satisfied_by(ex) implies
             tla_exists(at_after_create_pod).satisfied_by(ex) by {
                 let s = ex.head().ongoing_reconciles()[vrs.object_ref()].local_state;
                 let witness_n = choose |n: usize| s.reconcile_step == VReplicaSetReconcileStep::AfterCreatePod(n);
@@ -434,9 +434,9 @@ proof fn lemma_from_after_list_pods_to_reconcile_idle(
         lift_state(VRSCluster::at_expected_reconcile_states(vrs.object_ref(), |s: VReplicaSetReconcileState|
         exists |n: usize| s.reconcile_step == VReplicaSetReconcileStep::AfterDeletePod(n))),
         {
-            assert forall |ex| #![auto] 
+            assert forall |ex| #![auto]
             lift_state(VRSCluster::at_expected_reconcile_states(vrs.object_ref(), |s: VReplicaSetReconcileState|
-            exists |n: usize| s.reconcile_step == VReplicaSetReconcileStep::AfterDeletePod(n))).satisfied_by(ex) implies 
+            exists |n: usize| s.reconcile_step == VReplicaSetReconcileStep::AfterDeletePod(n))).satisfied_by(ex) implies
             tla_exists(at_after_delete_pod).satisfied_by(ex) by {
                 let s = ex.head().ongoing_reconciles()[vrs.object_ref()].local_state;
                 let witness_n = choose |n: usize| s.reconcile_step == VReplicaSetReconcileStep::AfterDeletePod(n);
@@ -461,7 +461,7 @@ proof fn lemma_from_after_list_pods_to_reconcile_idle(
 
 
     VRSCluster::lemma_from_some_state_to_arbitrary_next_state(spec, vrs, at_step_closure(VReplicaSetReconcileStep::AfterListPods), state_after_list_pods);
-    
+
     leads_to_trans_n!(
         spec,
         lift_state(at_step_state_pred(vrs, VReplicaSetReconcileStep::AfterListPods)),
@@ -471,7 +471,7 @@ proof fn lemma_from_after_list_pods_to_reconcile_idle(
 }
 
 proof fn lemma_true_equal_to_reconcile_idle_or_at_any_state(vrs: VReplicaSetView)
-    ensures true_pred::<VRSCluster>() 
+    ensures true_pred::<VRSCluster>()
                 == lift_state(|s: VRSCluster| { !s.ongoing_reconciles().contains_key(vrs.object_ref()) })
                     .or(lift_state(at_step_state_pred(vrs, VReplicaSetReconcileStep::Init)))
                     .or(lift_state(at_step_state_pred(vrs, VReplicaSetReconcileStep::AfterListPods)))
diff --git a/src/controller_examples/zookeeper_controller/proof/helper_invariants/proof.rs b/src/controller_examples/zookeeper_controller/proof/helper_invariants/proof.rs
index e68e1f2dc..52ad3e2e0 100644
--- a/src/controller_examples/zookeeper_controller/proof/helper_invariants/proof.rs
+++ b/src/controller_examples/zookeeper_controller/proof/helper_invariants/proof.rs
@@ -158,7 +158,7 @@ pub proof fn lemma_eventually_always_cm_rv_is_the_same_as_etcd_server_cm_if_cm_u
         lift_state(object_in_response_at_after_update_resource_step_is_same_as_etcd(SubResource::ConfigMap, zookeeper)),
         lift_state(object_in_every_resource_update_request_only_has_owner_references_pointing_to_current_cr(SubResource::ConfigMap, zookeeper))
     );
-    leads_to_weaken_temp(
+    leads_to_weaken(
         spec, true_pred(), lift_state(|s: ZKCluster| !s.ongoing_reconciles().contains_key(zookeeper.object_ref())),
         true_pred(), lift_state(inv)
     );
@@ -176,7 +176,7 @@ pub proof fn lemma_eventually_always_cm_rv_is_the_same_as_etcd_server_cm_if_cm_u
             }
         }
     }
-    leads_to_stable_temp(spec, lift_action(next), true_pred(), lift_state(inv));
+    leads_to_stable(spec, lift_action(next), true_pred(), lift_state(inv));
 }
 
 pub proof fn lemma_eventually_always_object_in_response_at_after_create_resource_step_is_same_as_etcd_forall(
@@ -254,7 +254,7 @@ pub proof fn lemma_eventually_always_object_in_response_at_after_create_resource
         lift_state(object_in_every_resource_update_request_only_has_owner_references_pointing_to_current_cr(SubResource::ConfigMap, zookeeper)),
         lift_state(resource_object_has_no_finalizers_or_timestamp_and_only_has_controller_owner_ref(SubResource::ConfigMap, zookeeper))
     );
-    leads_to_weaken_temp(
+    leads_to_weaken(
         spec, true_pred(), lift_state(|s: ZKCluster| !s.ongoing_reconciles().contains_key(zookeeper.object_ref())),
         true_pred(), lift_state(inv)
     );
@@ -327,7 +327,7 @@ pub proof fn lemma_eventually_always_object_in_response_at_after_create_resource
             }
         }
     }
-    leads_to_stable_temp(spec, lift_action(next), true_pred(), lift_state(inv));
+    leads_to_stable(spec, lift_action(next), true_pred(), lift_state(inv));
 }
 
 pub proof fn lemma_eventually_always_object_in_response_at_after_update_resource_step_is_same_as_etcd_forall(
@@ -405,7 +405,7 @@ pub proof fn lemma_eventually_always_object_in_response_at_after_update_resource
         lift_state(object_in_every_resource_update_request_only_has_owner_references_pointing_to_current_cr(SubResource::ConfigMap, zookeeper)),
         lift_state(resource_object_has_no_finalizers_or_timestamp_and_only_has_controller_owner_ref(SubResource::ConfigMap, zookeeper))
     );
-    leads_to_weaken_temp(
+    leads_to_weaken(
         spec, true_pred(), lift_state(|s: ZKCluster| !s.ongoing_reconciles().contains_key(zookeeper.object_ref())),
         true_pred(), lift_state(inv)
     );
@@ -479,7 +479,7 @@ pub proof fn lemma_eventually_always_object_in_response_at_after_update_resource
             }
         }
     }
-    leads_to_stable_temp(spec, lift_action(next), true_pred(), lift_state(inv));
+    leads_to_stable(spec, lift_action(next), true_pred(), lift_state(inv));
 }
 
 #[verifier(spinoff_prover)]
@@ -1347,7 +1347,7 @@ pub proof fn lemma_eventually_always_no_delete_resource_request_msg_in_flight(sp
         &&& resource_object_only_has_owner_reference_pointing_to_current_cr(sub_resource, zookeeper)(s)
         &&& resource_well_formed(s)
     };
-    always_weaken_temp(spec, lift_state(ZKCluster::each_object_in_etcd_is_well_formed()), lift_state(resource_well_formed));
+    always_weaken(spec, lift_state(ZKCluster::each_object_in_etcd_is_well_formed()), lift_state(resource_well_formed));
     assert forall |s: ZKCluster, s_prime: ZKCluster| #[trigger] stronger_next(s, s_prime) implies ZKCluster::every_new_req_msg_if_in_flight_then_satisfies(requirements)(s, s_prime) by {
         assert forall |msg: ZKMessage| (!s.in_flight().contains(msg) || requirements(msg, s)) && #[trigger] s_prime.in_flight().contains(msg)
         implies requirements(msg, s_prime) by {
@@ -1436,9 +1436,9 @@ pub proof fn lemma_eventually_always_resource_object_only_has_owner_reference_po
 {
     let key = get_request(sub_resource, zookeeper).key;
     let eventual_owner_ref = |owner_ref: Option<Seq<OwnerReferenceView>>| {owner_ref == Some(seq![zookeeper.controller_owner_ref()])};
-    always_weaken_temp(spec, lift_state(object_in_every_resource_update_request_only_has_owner_references_pointing_to_current_cr(sub_resource, zookeeper)), lift_state(ZKCluster::every_update_msg_sets_owner_references_as(key, eventual_owner_ref)));
-    always_weaken_temp(spec, lift_state(every_resource_create_request_implies_at_after_create_resource_step(sub_resource, zookeeper)), lift_state(ZKCluster::every_create_msg_sets_owner_references_as(key, eventual_owner_ref)));
-    always_weaken_temp(spec, lift_state(resource_object_has_no_finalizers_or_timestamp_and_only_has_controller_owner_ref(sub_resource, zookeeper)), lift_state(ZKCluster::object_has_no_finalizers(key)));
+    always_weaken(spec, lift_state(object_in_every_resource_update_request_only_has_owner_references_pointing_to_current_cr(sub_resource, zookeeper)), lift_state(ZKCluster::every_update_msg_sets_owner_references_as(key, eventual_owner_ref)));
+    always_weaken(spec, lift_state(every_resource_create_request_implies_at_after_create_resource_step(sub_resource, zookeeper)), lift_state(ZKCluster::every_create_msg_sets_owner_references_as(key, eventual_owner_ref)));
+    always_weaken(spec, lift_state(resource_object_has_no_finalizers_or_timestamp_and_only_has_controller_owner_ref(sub_resource, zookeeper)), lift_state(ZKCluster::object_has_no_finalizers(key)));
 
     let state = |s: ZKCluster| {
         ZKCluster::desired_state_is(zookeeper)(s)
diff --git a/src/controller_examples/zookeeper_controller/proof/helper_invariants/unchangeable.rs b/src/controller_examples/zookeeper_controller/proof/helper_invariants/unchangeable.rs
index be5e266e4..69c903808 100644
--- a/src/controller_examples/zookeeper_controller/proof/helper_invariants/unchangeable.rs
+++ b/src/controller_examples/zookeeper_controller/proof/helper_invariants/unchangeable.rs
@@ -156,7 +156,7 @@ pub proof fn lemma_always_object_in_etcd_satisfies_unchangeable(spec: TempPred<Z
         object_in_every_update_request_msg_satisfies_unchangeable_induction(sub_resource, zookeeper, s, s_prime);
     }
     init_invariant(spec, ZKCluster::init(), next, inv);
-    always_weaken_temp(spec, lift_state(inv), lift_state(object_in_etcd_satisfies_unchangeable(sub_resource, zookeeper)));
+    always_weaken(spec, lift_state(inv), lift_state(object_in_etcd_satisfies_unchangeable(sub_resource, zookeeper)));
 }
 
 pub proof fn object_in_etcd_satisfies_unchangeable_induction(sub_resource: SubResource, zookeeper: ZookeeperClusterView, s: ZKCluster, s_prime: ZKCluster)
diff --git a/src/controller_examples/zookeeper_controller/proof/liveness/proof.rs b/src/controller_examples/zookeeper_controller/proof/liveness/proof.rs
index 700ef5b62..a47214055 100644
--- a/src/controller_examples/zookeeper_controller/proof/liveness/proof.rs
+++ b/src/controller_examples/zookeeper_controller/proof/liveness/proof.rs
@@ -65,7 +65,7 @@ proof fn liveness_proof(zookeeper: ZookeeperClusterView)
     unpack_conditions_from_spec(invariants(zookeeper), assumption, true_pred(), always(lift_state(current_state_matches::<ZookeeperMaker>(zookeeper))));
     temp_pred_equality(true_pred().and(assumption), assumption);
 
-    valid_implies_trans(
+    entails_trans(
         cluster_spec().and(derived_invariants_since_beginning(zookeeper)), invariants(zookeeper),
         always(lift_state(ZKCluster::desired_state_is(zookeeper))).leads_to(always(lift_state(current_state_matches::<ZookeeperMaker>(zookeeper))))
     );
@@ -85,7 +85,7 @@ proof fn spec_before_phase_n_entails_true_leads_to_current_state_matches(i: nat,
     spec_of_previous_phases_entails_eventually_new_invariants(i, zookeeper);
     unpack_conditions_from_spec(spec_before_phase_n(i, zookeeper), invariants_since_phase_n(i, zookeeper), true_pred(), always(lift_state(current_state_matches::<ZookeeperMaker>(zookeeper))));
     temp_pred_equality(true_pred().and(invariants_since_phase_n(i, zookeeper)), invariants_since_phase_n(i, zookeeper));
-    leads_to_trans_temp(spec_before_phase_n(i, zookeeper), true_pred(), invariants_since_phase_n(i, zookeeper), always(lift_state(current_state_matches::<ZookeeperMaker>(zookeeper))));
+    leads_to_trans(spec_before_phase_n(i, zookeeper), true_pred(), invariants_since_phase_n(i, zookeeper), always(lift_state(current_state_matches::<ZookeeperMaker>(zookeeper))));
 }
 
 proof fn lemma_true_leads_to_always_current_state_matches(zookeeper: ZookeeperClusterView)
@@ -173,7 +173,7 @@ proof fn lemma_true_leads_to_always_state_matches_for_all_but_stateful_set(zooke
     ) by {
         always_tla_forall_apply_for_sub_resource(spec, sub_resource, zookeeper);
         lemma_from_after_get_resource_step_to_resource_matches(spec, zookeeper, sub_resource);
-        leads_to_trans_temp(
+        leads_to_trans(
             spec, true_pred(), lift_state(pending_req_in_flight_at_after_get_resource_step(sub_resource, zookeeper)),
             lift_state(sub_resource_state_matches(sub_resource, zookeeper))
         );
@@ -251,7 +251,7 @@ proof fn lemma_true_leads_to_always_state_matches_for_stateful_set(zookeeper: Zo
 
         // We then prove pending_req_in_flight_at_after_get_resource_step(SubResource::StatefulSet, zookeeper) ~> sub_resource_state_matches(SubResource::StatefulSet, zookeeper)
         lemma_from_after_get_stateful_set_step_to_stateful_set_matches(spec, zookeeper);
-        leads_to_trans_temp(
+        leads_to_trans(
             spec, true_pred(), lift_state(pending_req_in_flight_at_after_get_resource_step(SubResource::StatefulSet, zookeeper)),
             lift_state(sub_resource_state_matches(SubResource::StatefulSet, zookeeper))
         );
@@ -263,13 +263,13 @@ proof fn lemma_true_leads_to_always_state_matches_for_stateful_set(zookeeper: Zo
         unpack_conditions_from_spec(spec2, always(lift_state(helper_invariants::stateful_set_not_exists_or_matches_or_no_more_status_update(zookeeper))), true_pred(), always(lift_state(sub_resource_state_matches(SubResource::StatefulSet, zookeeper))));
         temp_pred_equality(always(lift_state(helper_invariants::stateful_set_not_exists_or_matches_or_no_more_status_update(zookeeper))), true_pred().and(always(lift_state(helper_invariants::stateful_set_not_exists_or_matches_or_no_more_status_update(zookeeper)))));
         helper_invariants::lemma_eventually_always_stateful_set_not_exists_or_matches_or_no_more_status_update(spec2, zookeeper);
-        leads_to_trans_temp(spec2, true_pred(), always(lift_state(helper_invariants::stateful_set_not_exists_or_matches_or_no_more_status_update(zookeeper))), always(lift_state(sub_resource_state_matches(SubResource::StatefulSet, zookeeper))));
+        leads_to_trans(spec2, true_pred(), always(lift_state(helper_invariants::stateful_set_not_exists_or_matches_or_no_more_status_update(zookeeper))), always(lift_state(sub_resource_state_matches(SubResource::StatefulSet, zookeeper))));
     });
 
     assert_by(spec1.entails(true_pred().leads_to(always(lift_state(sub_resource_state_matches(SubResource::StatefulSet, zookeeper))))), {
         unpack_conditions_from_spec(spec1, always(lift_state(sub_resource_state_matches(SubResource::ConfigMap, zookeeper))), true_pred(), always(lift_state(sub_resource_state_matches(SubResource::StatefulSet, zookeeper))));
         temp_pred_equality(always(lift_state(sub_resource_state_matches(SubResource::ConfigMap, zookeeper))), true_pred().and(always(lift_state(sub_resource_state_matches(SubResource::ConfigMap, zookeeper)))));
-        leads_to_trans_temp(spec1, true_pred(), always(lift_state(sub_resource_state_matches(SubResource::ConfigMap, zookeeper))), always(lift_state(sub_resource_state_matches(SubResource::StatefulSet, zookeeper))));
+        leads_to_trans(spec1, true_pred(), always(lift_state(sub_resource_state_matches(SubResource::ConfigMap, zookeeper))), always(lift_state(sub_resource_state_matches(SubResource::StatefulSet, zookeeper))));
     });
 }
 
@@ -294,9 +294,25 @@ proof fn lemma_from_reconcile_idle_to_scheduled(spec: TempPred<ZKCluster>, zooke
         &&& s.scheduled_reconciles().contains_key(zookeeper.object_ref())
     };
     let input = zookeeper.object_ref();
-    ZKCluster::lemma_pre_leads_to_post_by_schedule_controller_reconcile_borrow_from_spec(spec, input, ZKCluster::next(), ZKCluster::desired_state_is(zookeeper), pre, post);
-    valid_implies_implies_leads_to(spec, lift_state(post), lift_state(post));
-    or_leads_to_combine_temp(spec, lift_state(pre), lift_state(post), lift_state(post));
+    let stronger_pre = |s| {
+        &&& pre(s)
+        &&& desired_state_is(zookeeper)(s)
+    };
+    let stronger_next = |s, s_prime| {
+        &&& ZKCluster::next()(s, s_prime)
+        &&& desired_state_is(zookeeper)(s_prime)
+    };
+    always_to_always_later(spec, lift_state(desired_state_is(zookeeper)));
+    combine_spec_entails_always_n!(
+        spec, lift_action(stronger_next),
+        lift_action(ZKCluster::next()),
+        later(lift_state(desired_state_is(zookeeper)))
+    );
+    ZKCluster::lemma_pre_leads_to_post_by_schedule_controller_reconcile(spec, input, stronger_next, stronger_pre, post);
+    temp_pred_equality(lift_state(pre).and(lift_state(desired_state_is(zookeeper))), lift_state(stronger_pre));
+    leads_to_by_borrowing_inv(spec, lift_state(pre), lift_state(post), lift_state(desired_state_is(zookeeper)));
+    entails_implies_leads_to(spec, lift_state(post), lift_state(post));
+    or_leads_to_combine(spec, lift_state(pre), lift_state(post), lift_state(post));
     temp_pred_equality(lift_state(pre).or(lift_state(post)), lift_state(|s: ZKCluster| {!s.ongoing_reconciles().contains_key(zookeeper.object_ref())}));
 }
 
diff --git a/src/controller_examples/zookeeper_controller/proof/liveness/resource_match.rs b/src/controller_examples/zookeeper_controller/proof/liveness/resource_match.rs
index 53a57c2a3..9fbc73f70 100644
--- a/src/controller_examples/zookeeper_controller/proof/liveness/resource_match.rs
+++ b/src/controller_examples/zookeeper_controller/proof/liveness/resource_match.rs
@@ -72,7 +72,7 @@ pub proof fn lemma_from_after_get_resource_step_to_resource_matches(
         &&& s.resources().contains_key(get_request(sub_resource, zookeeper).key)
         &&& pending_req_in_flight_at_after_get_resource_step(sub_resource, zookeeper)(s)
     });
-    or_leads_to_combine_temp(spec, key_not_exists, key_exists, lift_state(sub_resource_state_matches(sub_resource, zookeeper)));
+    or_leads_to_combine(spec, key_not_exists, key_exists, lift_state(sub_resource_state_matches(sub_resource, zookeeper)));
     temp_pred_equality(
         key_not_exists.or(key_exists), lift_state(pending_req_in_flight_at_after_get_resource_step(sub_resource, zookeeper))
     );
@@ -82,7 +82,7 @@ pub proof fn lemma_from_after_get_resource_step_to_resource_matches(
     } else {
         pending_req_in_flight_at_after_exists_stateful_set_step(zookeeper) // ConfigMap is a bit different since its next step is not a SubResource type
     };
-    or_leads_to_combine_temp(spec, key_not_exists, key_exists, lift_state(next_state));
+    or_leads_to_combine(spec, key_not_exists, key_exists, lift_state(next_state));
 }
 
 pub proof fn lemma_from_after_get_resource_step_and_key_not_exists_to_resource_matches(
@@ -201,7 +201,7 @@ pub proof fn lemma_from_after_get_resource_step_and_key_not_exists_to_resource_m
     });
 
     assert_by(spec.entails(pre.leads_to(lift_state(sub_resource_state_matches(sub_resource, zookeeper)))), {
-        valid_implies_implies_leads_to(spec, match_and_ok_resp, lift_state(sub_resource_state_matches(sub_resource, zookeeper)));
+        entails_implies_leads_to(spec, match_and_ok_resp, lift_state(sub_resource_state_matches(sub_resource, zookeeper)));
         leads_to_trans_n!(spec, pre, match_and_ok_resp, lift_state(sub_resource_state_matches(sub_resource, zookeeper)));
     });
 
@@ -262,7 +262,7 @@ pub proof fn lemma_from_after_get_resource_step_and_key_not_exists_to_resource_m
                 }
                 temp_pred_equality(tla_exists(known_ok_resp), exists_ok_resp);
             });
-            valid_implies_implies_leads_to(spec, match_and_ok_resp, exists_ok_resp);
+            entails_implies_leads_to(spec, match_and_ok_resp, exists_ok_resp);
             leads_to_trans_n!(spec, pre, match_and_ok_resp, exists_ok_resp, lift_state(next_state));
         });
     }
@@ -375,7 +375,7 @@ proof fn lemma_from_after_get_resource_step_and_key_exists_to_resource_matches(
     });
 
     assert_by(spec.entails(pre.leads_to(lift_state(sub_resource_state_matches(sub_resource, zookeeper)))), {
-        valid_implies_implies_leads_to(spec, match_and_ok_resp, lift_state(sub_resource_state_matches(sub_resource, zookeeper)));
+        entails_implies_leads_to(spec, match_and_ok_resp, lift_state(sub_resource_state_matches(sub_resource, zookeeper)));
         leads_to_trans_n!(spec, pre, match_and_ok_resp, lift_state(sub_resource_state_matches(sub_resource, zookeeper)));
     });
 
@@ -433,7 +433,7 @@ proof fn lemma_from_after_get_resource_step_and_key_exists_to_resource_matches(
             }
             temp_pred_equality(tla_exists(known_ok_resp), exists_ok_resp);
         });
-        valid_implies_implies_leads_to(spec, match_and_ok_resp, exists_ok_resp);
+        entails_implies_leads_to(spec, match_and_ok_resp, exists_ok_resp);
         leads_to_trans_n!(spec, pre, match_and_ok_resp, exists_ok_resp, lift_state(next_state));
     });
 }
@@ -1005,7 +1005,7 @@ pub proof fn lemma_resource_object_is_stable(spec: TempPred<ZKCluster>, sub_reso
         }
     }
 
-    leads_to_stable_temp(spec, lift_action(stronger_next), p, lift_state(post));
+    leads_to_stable(spec, lift_action(stronger_next), p, lift_state(post));
 }
 
 }
diff --git a/src/controller_examples/zookeeper_controller/proof/liveness/stateful_set_match.rs b/src/controller_examples/zookeeper_controller/proof/liveness/stateful_set_match.rs
index 8e105a91d..d0a8897ee 100644
--- a/src/controller_examples/zookeeper_controller/proof/liveness/stateful_set_match.rs
+++ b/src/controller_examples/zookeeper_controller/proof/liveness/stateful_set_match.rs
@@ -62,7 +62,7 @@ pub proof fn lemma_from_after_get_stateful_set_step_to_stateful_set_matches(
         &&& s.resources().contains_key(get_request(SubResource::StatefulSet, zookeeper).key)
         &&& pending_req_in_flight_at_after_get_resource_step(SubResource::StatefulSet, zookeeper)(s)
     });
-    or_leads_to_combine_temp(spec, key_not_exists, key_exists, lift_state(sub_resource_state_matches(SubResource::StatefulSet, zookeeper)));
+    or_leads_to_combine(spec, key_not_exists, key_exists, lift_state(sub_resource_state_matches(SubResource::StatefulSet, zookeeper)));
     temp_pred_equality(
         key_not_exists.or(key_exists), lift_state(pending_req_in_flight_at_after_get_resource_step(SubResource::StatefulSet, zookeeper))
     );
@@ -117,7 +117,7 @@ proof fn lemma_from_after_get_stateful_set_step_and_key_exists_to_stateful_set_m
     let post = lift_state(sub_resource_state_matches(SubResource::StatefulSet, zookeeper));
 
     assert_by(spec.entails(stateful_set_matches.leads_to(post)), {
-        valid_implies_implies_leads_to(spec, stateful_set_matches, post);
+        entails_implies_leads_to(spec, stateful_set_matches, post);
     });
 
     assert_by(spec.entails(stateful_set_not_matches.leads_to(post)), {
@@ -188,7 +188,7 @@ proof fn lemma_from_after_get_stateful_set_step_and_key_exists_to_stateful_set_m
         leads_to_trans_n!(spec, stateful_set_not_matches, post1, post2, post);
     });
 
-    or_leads_to_combine_temp(spec, stateful_set_matches, stateful_set_not_matches, post);
+    or_leads_to_combine(spec, stateful_set_matches, stateful_set_not_matches, post);
     temp_pred_equality(stateful_set_matches.or(stateful_set_not_matches), pre);
 }
 
@@ -526,7 +526,7 @@ pub proof fn lemma_stateful_set_is_stable(
         }
     }
 
-    leads_to_stable_temp(spec, lift_action(stronger_next), p, lift_state(post));
+    leads_to_stable(spec, lift_action(stronger_next), p, lift_state(post));
 }
 
 }
diff --git a/src/controller_examples/zookeeper_controller/proof/liveness/terminate.rs b/src/controller_examples/zookeeper_controller/proof/liveness/terminate.rs
index c08187ca2..c06d1b3e5 100644
--- a/src/controller_examples/zookeeper_controller/proof/liveness/terminate.rs
+++ b/src/controller_examples/zookeeper_controller/proof/liveness/terminate.rs
@@ -61,7 +61,7 @@ pub proof fn reconcile_eventually_terminates(spec: TempPred<ZKCluster>, zookeepe
     ZKCluster::lemma_reconcile_done_leads_to_reconcile_idle(spec, zookeeper.object_ref());
     temp_pred_equality(lift_state(at_step_state_pred(zookeeper, ZookeeperReconcileStep::Done)), lift_state(ZKCluster::reconciler_reconcile_done(zookeeper.object_ref())));
     temp_pred_equality(lift_state(at_step_state_pred(zookeeper, ZookeeperReconcileStep::Error)), lift_state(ZKCluster::reconciler_reconcile_error(zookeeper.object_ref())));
-    valid_implies_implies_leads_to(spec, lift_state(reconcile_idle), lift_state(reconcile_idle));
+    entails_implies_leads_to(spec, lift_state(reconcile_idle), lift_state(reconcile_idle));
 
     or_leads_to_combine_and_equality!(spec,
         lift_state(at_step1_or_step2_state_pred(zookeeper, ZookeeperReconcileStep::Done, ZookeeperReconcileStep::Error)),
diff --git a/src/controller_examples/zookeeper_controller/proof/liveness/zookeeper_api.rs b/src/controller_examples/zookeeper_controller/proof/liveness/zookeeper_api.rs
index 8ac9c398f..8eb865521 100644
--- a/src/controller_examples/zookeeper_controller/proof/liveness/zookeeper_api.rs
+++ b/src/controller_examples/zookeeper_controller/proof/liveness/zookeeper_api.rs
@@ -65,7 +65,7 @@ pub proof fn lemma_from_after_exists_stateful_set_step_to_after_get_stateful_set
         &&& s.resources().contains_key(get_request(SubResource::StatefulSet, zookeeper).key)
         &&& pending_req_in_flight_at_after_exists_stateful_set_step(zookeeper)(s)
     });
-    or_leads_to_combine_temp(spec, key_not_exists, key_exists, lift_state(pending_req_in_flight_at_after_get_resource_step(SubResource::StatefulSet, zookeeper)));
+    or_leads_to_combine(spec, key_not_exists, key_exists, lift_state(pending_req_in_flight_at_after_get_resource_step(SubResource::StatefulSet, zookeeper)));
     temp_pred_equality(key_not_exists.or(key_exists), lift_state(pending_req_in_flight_at_after_exists_stateful_set_step(zookeeper)));
 }
 
@@ -230,7 +230,7 @@ proof fn lemma_from_after_exists_stateful_set_step_and_key_exists_to_after_get_s
             temp_pred_equality(tla_exists(after_exists_stateful_set_step_resp_msg), after_exists_stateful_set_step_waiting);
         });
 
-        leads_to_trans_temp(spec, pre, after_exists_stateful_set_step_waiting, after_exists_zk_node_step_pending);
+        leads_to_trans(spec, pre, after_exists_stateful_set_step_waiting, after_exists_zk_node_step_pending);
     });
 
     assert_by(spec.entails(after_exists_zk_node_step_pending.leads_to(post)) , {
@@ -483,10 +483,10 @@ proof fn lemma_from_after_exists_stateful_set_step_and_key_exists_to_after_get_s
             );
         });
 
-        or_leads_to_combine_temp(spec, addr_exists_and_after_exists_zk_node_step_pending, addr_not_exists_and_after_exists_zk_node_step_pending, post);
+        or_leads_to_combine(spec, addr_exists_and_after_exists_zk_node_step_pending, addr_not_exists_and_after_exists_zk_node_step_pending, post);
         temp_pred_equality(addr_exists_and_after_exists_zk_node_step_pending.or(addr_not_exists_and_after_exists_zk_node_step_pending), after_exists_zk_node_step_pending);
     });
-    leads_to_trans_temp(spec, pre, after_exists_zk_node_step_pending, post);
+    leads_to_trans(spec, pre, after_exists_zk_node_step_pending, post);
 }
 
 proof fn lemma_from_pending_req_to_receives_not_found_resp_at_after_exists_stateful_set_step(spec: TempPred<ZKCluster>, zookeeper: ZookeeperClusterView, req_msg: ZKMessage)
diff --git a/src/kubernetes_cluster/proof/api_server_liveness.rs b/src/kubernetes_cluster/proof/api_server_liveness.rs
index ef1423399..e8fcdd67a 100644
--- a/src/kubernetes_cluster/proof/api_server_liveness.rs
+++ b/src/kubernetes_cluster/proof/api_server_liveness.rs
@@ -33,7 +33,7 @@ pub proof fn lemma_pre_leads_to_post_by_kubernetes_api(
 {
     use_tla_forall::<Self, Option<MsgType<E>>>(spec, |i| Self::kubernetes_api_next().weak_fairness(i), input);
     Self::kubernetes_api_action_pre_implies_next_pre(action, input);
-    valid_implies_trans::<Self>(
+    entails_trans::<Self>(
         lift_state(pre),
         lift_state(Self::kubernetes_api_action_pre(action, input)),
         lift_state(Self::kubernetes_api_next().pre(input))
@@ -55,7 +55,7 @@ pub proof fn lemma_pre_leads_to_post_by_builtin_controllers(
 {
     use_tla_forall::<Self, (BuiltinControllerChoice, ObjectRef)>(spec, |i| Self::builtin_controllers_next().weak_fairness(i), input);
     Self::builtin_controllers_action_pre_implies_next_pre(action, input);
-    valid_implies_trans::<Self>(
+    entails_trans::<Self>(
         lift_state(pre),
         lift_state(Self::builtin_controllers_action_pre(action, input)),
         lift_state(Self::builtin_controllers_next().pre(input))
@@ -238,17 +238,17 @@ pub proof fn lemma_some_rest_id_leads_to_always_every_in_flight_req_msg_satisfie
 
             Self::lemma_true_leads_to_always_no_req_before_rest_id_is_in_flight(spec_with_rest_id, rest_id);
 
-            implies_preserved_by_always_temp(
+            entails_preserved_by_always(
                 lift_state(invariant),
                 lift_state(Self::no_req_before_rest_id_is_in_flight(rest_id))
                 .implies(lift_state(Self::every_in_flight_req_msg_satisfies(requirements)))
             );
-            valid_implies_trans(
+            entails_trans(
                 spec_with_rest_id, always(lift_state(invariant)),
                 always(lift_state(Self::no_req_before_rest_id_is_in_flight(rest_id)).implies(lift_state(Self::every_in_flight_req_msg_satisfies(requirements))))
             );
-            always_implies_preserved_by_always_temp(spec_with_rest_id, lift_state(Self::no_req_before_rest_id_is_in_flight(rest_id)), lift_state(Self::every_in_flight_req_msg_satisfies(requirements)));
-            leads_to_weaken_temp(
+            always_implies_preserved_by_always(spec_with_rest_id, lift_state(Self::no_req_before_rest_id_is_in_flight(rest_id)), lift_state(Self::every_in_flight_req_msg_satisfies(requirements)));
+            leads_to_weaken(
                 spec_with_rest_id,
                 true_pred(), always(lift_state(Self::no_req_before_rest_id_is_in_flight(rest_id))),
                 true_pred(), always(lift_state(Self::every_in_flight_req_msg_satisfies(requirements)))
@@ -262,7 +262,7 @@ pub proof fn lemma_some_rest_id_leads_to_always_every_in_flight_req_msg_satisfie
         always(lift_state(Self::every_in_flight_req_msg_satisfies(requirements)))
     );
     temp_pred_equality(true_pred().and(lift_state(Self::rest_id_counter_is(rest_id))), lift_state(Self::rest_id_counter_is(rest_id)));
-    valid_implies_trans(spec, stable_spec, lift_state(Self::rest_id_counter_is(rest_id)).leads_to(always(lift_state(Self::every_in_flight_req_msg_satisfies(requirements)))));
+    entails_trans(spec, stable_spec, lift_state(Self::rest_id_counter_is(rest_id)).leads_to(always(lift_state(Self::every_in_flight_req_msg_satisfies(requirements)))));
 }
 
 // All the APIRequest messages with a smaller id than rest_id will eventually leave the network.
@@ -293,7 +293,7 @@ pub proof fn lemma_true_leads_to_always_no_req_before_rest_id_is_in_flight(spec:
         }
     }
 
-    leads_to_stable_temp(spec, lift_action(stronger_next), true_pred(), lift_state(Self::no_req_before_rest_id_is_in_flight(rest_id)));
+    leads_to_stable(spec, lift_action(stronger_next), true_pred(), lift_state(Self::no_req_before_rest_id_is_in_flight(rest_id)));
 }
 
 pub proof fn lemma_eventually_no_req_before_rest_id_is_in_flight(spec: TempPred<Self>, rest_id: RestId)
@@ -357,7 +357,7 @@ proof fn lemma_pending_requests_number_is_n_leads_to_no_pending_requests(spec: T
                 }
             }
         });
-        valid_implies_implies_leads_to(spec, lift_state(pending_requests_num_is_zero), lift_state(no_more_pending_requests));
+        entails_implies_leads_to(spec, lift_state(pending_requests_num_is_zero), lift_state(no_more_pending_requests));
     } else {
         // The induction step:
         // If we already have "there are msg_num-1 such requests" ~> "all such requests are gone" (the inductive hypothesis),
@@ -406,7 +406,7 @@ proof fn lemma_pending_requests_number_is_n_leads_to_no_pending_requests(spec: T
         Self::lemma_pending_requests_number_is_n_leads_to_no_pending_requests(
             spec, rest_id, (msg_num - 1) as nat
         );
-        leads_to_trans_temp(
+        leads_to_trans(
             spec, pending_requests_num_is_msg_num, pending_requests_num_is_msg_num_minus_1, no_more_pending_requests
         );
     }
diff --git a/src/kubernetes_cluster/proof/builtin_controllers.rs b/src/kubernetes_cluster/proof/builtin_controllers.rs
index 220e43d5c..ac43ab471 100644
--- a/src/kubernetes_cluster/proof/builtin_controllers.rs
+++ b/src/kubernetes_cluster/proof/builtin_controllers.rs
@@ -208,7 +208,7 @@ pub proof fn lemma_eventually_objects_owner_references_satisfies(
             leads_to_trans_n!(spec, lift_state(pre), lift_state(delete_msg_in_flight), lift_state(post));
 
             temp_pred_equality(lift_state(Self::objects_owner_references_violates(key, eventual_owner_ref)).implies(lift_state(Self::garbage_collector_deletion_enabled(key))), lift_state(Self::objects_owner_references_violates(key, eventual_owner_ref)).implies(lift_state(pre)));
-            leads_to_weaken_temp(spec, lift_state(pre), lift_state(post), lift_state(Self::objects_owner_references_violates(key, eventual_owner_ref)), lift_state(post));
+            leads_to_weaken(spec, lift_state(pre), lift_state(post), lift_state(Self::objects_owner_references_violates(key, eventual_owner_ref)), lift_state(post));
         }
     );
 
@@ -227,7 +227,7 @@ pub proof fn lemma_eventually_objects_owner_references_satisfies(
         }
     }
 
-    leads_to_stable_temp(spec, lift_action(stronger_next), true_pred(), lift_state(post));
+    leads_to_stable(spec, lift_action(stronger_next), true_pred(), lift_state(post));
 }
 
 proof fn lemma_delete_msg_in_flight_leads_to_owner_references_satisfies(
diff --git a/src/kubernetes_cluster/proof/cluster.rs b/src/kubernetes_cluster/proof/cluster.rs
index 8c03ac966..69b33f388 100644
--- a/src/kubernetes_cluster/proof/cluster.rs
+++ b/src/kubernetes_cluster/proof/cluster.rs
@@ -59,7 +59,7 @@ pub proof fn lemma_true_leads_to_crash_always_disabled(
 {
     let true_state = |s: Self| true;
     Self::disable_crash().wf1((), spec, Self::next(), true_state, Self::crash_disabled());
-    leads_to_stable_temp::<Self>(spec, lift_action(Self::next()), true_pred(), lift_state(Self::crash_disabled()));
+    leads_to_stable::<Self>(spec, lift_action(Self::next()), true_pred(), lift_state(Self::crash_disabled()));
 }
 
 pub proof fn lemma_true_leads_to_busy_always_disabled(
@@ -72,7 +72,7 @@ pub proof fn lemma_true_leads_to_busy_always_disabled(
 {
     let true_state = |s: Self| true;
     Self::disable_transient_failure().wf1((), spec, Self::next(), true_state, Self::busy_disabled());
-    leads_to_stable_temp::<Self>(spec, lift_action(Self::next()), true_pred(), lift_state(Self::busy_disabled()));
+    leads_to_stable::<Self>(spec, lift_action(Self::next()), true_pred(), lift_state(Self::busy_disabled()));
 }
 
 // This desired_state_is specifies the desired state (described in the cr object)
diff --git a/src/kubernetes_cluster/proof/controller_runtime_eventual_safety.rs b/src/kubernetes_cluster/proof/controller_runtime_eventual_safety.rs
index 273ae2a8f..a66c739df 100644
--- a/src/kubernetes_cluster/proof/controller_runtime_eventual_safety.rs
+++ b/src/kubernetes_cluster/proof/controller_runtime_eventual_safety.rs
@@ -39,17 +39,28 @@ pub proof fn lemma_true_leads_to_always_the_object_in_schedule_has_spec_and_uid_
     let pre = |s: Self| true;
     let post = Self::the_object_in_schedule_has_spec_and_uid_as(cr);
     let input = cr.object_ref();
-    let stronger_next = |s, s_prime: Self| {
-        &&& Self::next()(s, s_prime)
-        &&& Self::desired_state_is(cr)(s)
-    };
-    combine_spec_entails_always_n!(spec, lift_action(stronger_next), lift_action(Self::next()), lift_state(Self::desired_state_is(cr)));
 
     K::object_ref_is_well_formed();
-    Self::lemma_pre_leads_to_post_by_schedule_controller_reconcile_borrow_from_spec(
-        spec, input, stronger_next, Self::desired_state_is(cr), pre, post
+
+    let stronger_pre = |s| {
+        &&& pre(s)
+        &&& Self::desired_state_is(cr)(s)
+    };
+    let stronger_next = |s, s_prime| {
+        &&& Self::next()(s, s_prime)
+        &&& Self::desired_state_is(cr)(s_prime)
+    };
+    always_to_always_later(spec, lift_state(Self::desired_state_is(cr)));
+    combine_spec_entails_always_n!(
+        spec, lift_action(stronger_next),
+        lift_action(Self::next()),
+        later(lift_state(Self::desired_state_is(cr)))
     );
-    leads_to_stable_temp(spec, lift_action(stronger_next), lift_state(pre), lift_state(post));
+    Self::lemma_pre_leads_to_post_by_schedule_controller_reconcile(spec, input, stronger_next, stronger_pre, post);
+    temp_pred_equality(lift_state(pre).and(lift_state(Self::desired_state_is(cr))), lift_state(stronger_pre));
+    leads_to_by_borrowing_inv(spec, lift_state(pre), lift_state(post), lift_state(Self::desired_state_is(cr)));
+
+    leads_to_stable(spec, lift_action(stronger_next), lift_state(pre), lift_state(post));
 }
 
 pub open spec fn the_object_in_reconcile_has_spec_and_uid_as(cr: K) -> StatePred<Self> {
@@ -91,9 +102,27 @@ pub proof fn lemma_true_leads_to_always_the_object_in_reconcile_has_spec_and_uid
         {
             let input = cr.object_ref();
             K::object_ref_is_well_formed();
-            Self::lemma_pre_leads_to_post_by_schedule_controller_reconcile_borrow_from_spec(
-                spec, input, stronger_next, Self::desired_state_is(cr), not_scheduled_or_reconcile, scheduled_and_not_reconcile
+
+            let pre = not_scheduled_or_reconcile;
+            let post = scheduled_and_not_reconcile;
+            let stronger_pre = |s| {
+                &&& pre(s)
+                &&& Self::desired_state_is(cr)(s)
+            };
+            let even_stronger_next = |s, s_prime| {
+                &&& stronger_next(s, s_prime)
+                &&& Self::desired_state_is(cr)(s_prime)
+            };
+            always_to_always_later(spec, lift_state(Self::desired_state_is(cr)));
+            combine_spec_entails_always_n!(
+                spec, lift_action(even_stronger_next),
+                lift_action(stronger_next),
+                later(lift_state(Self::desired_state_is(cr)))
             );
+            Self::lemma_pre_leads_to_post_by_schedule_controller_reconcile(spec, input, even_stronger_next, stronger_pre, post);
+            temp_pred_equality(lift_state(pre).and(lift_state(Self::desired_state_is(cr))), lift_state(stronger_pre));
+            leads_to_by_borrowing_inv(spec, lift_state(pre), lift_state(post), lift_state(Self::desired_state_is(cr)));
+
         }
     );
     assert_by(
@@ -107,7 +136,7 @@ pub proof fn lemma_true_leads_to_always_the_object_in_reconcile_has_spec_and_uid
             );
         }
     );
-    leads_to_trans_temp(spec, lift_state(not_scheduled_or_reconcile), lift_state(scheduled_and_not_reconcile), lift_state(Self::the_object_in_reconcile_has_spec_and_uid_as(cr)));
+    leads_to_trans(spec, lift_state(not_scheduled_or_reconcile), lift_state(scheduled_and_not_reconcile), lift_state(Self::the_object_in_reconcile_has_spec_and_uid_as(cr)));
     let not_reconcile = |s: Self| !s.ongoing_reconciles().contains_key(cr.object_ref());
 
     or_leads_to_combine_and_equality!(
@@ -115,11 +144,11 @@ pub proof fn lemma_true_leads_to_always_the_object_in_reconcile_has_spec_and_uid
         lift_state(Self::the_object_in_reconcile_has_spec_and_uid_as(cr))
     );
 
-    leads_to_trans_temp(
+    leads_to_trans(
         spec, true_pred(), lift_state(|s: Self| !s.ongoing_reconciles().contains_key(cr.object_ref())),
         lift_state(Self::the_object_in_reconcile_has_spec_and_uid_as(cr))
     );
-    leads_to_stable_temp(spec, lift_action(stronger_next), true_pred(), lift_state(Self::the_object_in_reconcile_has_spec_and_uid_as(cr)));
+    leads_to_stable(spec, lift_action(stronger_next), true_pred(), lift_state(Self::the_object_in_reconcile_has_spec_and_uid_as(cr)));
 }
 
 }
diff --git a/src/kubernetes_cluster/proof/controller_runtime_liveness.rs b/src/kubernetes_cluster/proof/controller_runtime_liveness.rs
index 5c2d2af38..b06d60c8b 100644
--- a/src/kubernetes_cluster/proof/controller_runtime_liveness.rs
+++ b/src/kubernetes_cluster/proof/controller_runtime_liveness.rs
@@ -36,7 +36,7 @@ pub proof fn lemma_pre_leads_to_post_by_controller(
     );
 
     Self::controller_action_pre_implies_next_pre(action, input);
-    valid_implies_trans::<Self>(
+    entails_trans::<Self>(
         lift_state(pre),
         lift_state(Self::controller_action_pre(action, input)),
         lift_state(Self::controller_next().pre(input))
@@ -63,24 +63,6 @@ pub proof fn lemma_pre_leads_to_post_by_schedule_controller_reconcile(
     Self::schedule_controller_reconcile().wf1(input, spec, next, pre, post);
 }
 
-pub proof fn lemma_pre_leads_to_post_by_schedule_controller_reconcile_borrow_from_spec(
-    spec: TempPred<Self>, input: ObjectRef, next: ActionPred<Self>, c: StatePred<Self>, pre: StatePred<Self>, post: StatePred<Self>
-)
-    requires
-        forall |s, s_prime: Self| pre(s) && c(s) && #[trigger] next(s, s_prime) ==> pre(s_prime) || post(s_prime),
-        forall |s, s_prime: Self| pre(s) && c(s) && #[trigger] next(s, s_prime) && Self::schedule_controller_reconcile().forward(input)(s, s_prime) ==> post(s_prime),
-        forall |s: Self| #[trigger] pre(s) && c(s) ==> Self::schedule_controller_reconcile().pre(input)(s),
-        spec.entails(always(lift_action(next))),
-        spec.entails(tla_forall(|i| Self::schedule_controller_reconcile().weak_fairness(i))),
-        spec.entails(always(lift_state(c))),
-    ensures spec.entails(lift_state(pre).leads_to(lift_state(post))),
-{
-    use_tla_forall::<Self, ObjectRef>(
-        spec, |i| Self::schedule_controller_reconcile().weak_fairness(i), input
-    );
-    Self::schedule_controller_reconcile().wf1_borrow_from_spec(input, spec, next, c, pre, post);
-}
-
 pub proof fn lemma_reconcile_done_leads_to_reconcile_idle(spec: TempPred<Self>, cr_key: ObjectRef)
     requires
         K::kind().is_CustomResourceKind(),
@@ -261,7 +243,7 @@ pub proof fn lemma_from_some_state_to_arbitrary_next_state(
         })
     };
     temp_pred_equality::<Self>(lift_state(Self::pending_req_in_flight_or_resp_in_flight_at_reconcile_state(cr.object_ref(), state)), lift_state(Self::at_expected_reconcile_states(cr.object_ref(), state)).implies(lift_state(at_some_state_and_pending_req_in_flight_or_resp_in_flight)));
-    implies_to_leads_to::<Self>(spec, lift_state(Self::at_expected_reconcile_states(cr.object_ref(), state)), lift_state(at_some_state_and_pending_req_in_flight_or_resp_in_flight));
+    always_implies_to_leads_to::<Self>(spec, lift_state(Self::at_expected_reconcile_states(cr.object_ref(), state)), lift_state(at_some_state_and_pending_req_in_flight_or_resp_in_flight));
 
     let req_in_flight = Self::pending_req_in_flight_at_reconcile_state(cr.object_ref(), state);
     let resp_in_flight = Self::resp_in_flight_matches_pending_req_at_reconcile_state(cr.object_ref(), state);
@@ -269,7 +251,7 @@ pub proof fn lemma_from_some_state_to_arbitrary_next_state(
     Self::lemma_from_in_flight_resp_matches_pending_req_at_some_state_to_next_state(spec, cr, state, next_state);
     Self::lemma_from_pending_req_in_flight_at_some_state_to_next_state(spec, cr, state, next_state);
 
-    or_leads_to_combine_temp(spec, lift_state(req_in_flight), lift_state(resp_in_flight), lift_state(Self::at_expected_reconcile_states(cr.object_ref(), next_state)));
+    or_leads_to_combine(spec, lift_state(req_in_flight), lift_state(resp_in_flight), lift_state(Self::at_expected_reconcile_states(cr.object_ref(), next_state)));
     temp_pred_equality::<Self>(
         lift_state(req_in_flight).or(lift_state(resp_in_flight)),
         lift_state(at_some_state_and_pending_req_in_flight_or_resp_in_flight)
@@ -310,7 +292,7 @@ pub proof fn lemma_from_init_state_to_next_state_to_reconcile_idle(
         lift_state(Self::no_pending_req_msg_at_reconcile_state(cr.object_ref(), init_state)),
         lift_state(Self::at_expected_reconcile_states(cr.object_ref(), init_state)).implies(lift_state(no_pending_req))
     );
-    implies_to_leads_to(
+    always_implies_to_leads_to(
         spec,
         lift_state(Self::at_expected_reconcile_states(cr.object_ref(), init_state)),
         lift_state(no_pending_req)
@@ -569,7 +551,7 @@ pub proof fn lemma_from_some_state_with_ext_resp_to_two_next_states_to_reconcile
         && Self::no_pending_req_msg(s, cr.object_ref())
     };
     temp_pred_equality(lift_state(Self::no_pending_req_msg_at_reconcile_state(cr.object_ref(), state)), lift_state(Self::at_expected_reconcile_states(cr.object_ref(), state)).implies(lift_state(no_req_at_state)));
-    implies_to_leads_to(spec, lift_state(Self::at_expected_reconcile_states(cr.object_ref(), state)), lift_state(no_req_at_state));
+    always_implies_to_leads_to(spec, lift_state(Self::at_expected_reconcile_states(cr.object_ref(), state)), lift_state(no_req_at_state));
 
     let stronger_next = |s, s_prime: Self| {
         &&& Self::next()(s, s_prime)
diff --git a/src/kubernetes_cluster/proof/daemon_set_controller.rs b/src/kubernetes_cluster/proof/daemon_set_controller.rs
index f7e3afd52..ec75bee05 100644
--- a/src/kubernetes_cluster/proof/daemon_set_controller.rs
+++ b/src/kubernetes_cluster/proof/daemon_set_controller.rs
@@ -135,7 +135,7 @@ pub proof fn lemma_true_leads_to_always_daemon_set_not_exist_or_updated_or_no_mo
         }
     }
 
-    leads_to_stable_temp(spec, lift_action(stronger_next), true_pred(), lift_state(post));
+    leads_to_stable(spec, lift_action(stronger_next), true_pred(), lift_state(post));
 }
 
 proof fn lemma_true_leads_to_daemon_set_not_exist_or_updated_or_no_more_pending_req(spec: TempPred<Self>, key: ObjectRef, make_fn: spec_fn() -> DaemonSetView)
@@ -186,12 +186,12 @@ proof fn lemma_true_leads_to_daemon_set_not_exist_or_updated_or_no_more_pending_
         });
         temp_pred_equality(lift_state(|s: Self| s.stable_resources().contains(key)).or(lift_state(key_not_exists)), lift_state(key_not_exists_or_stable));
         temp_pred_equality(lift_state(post).or(lift_state(key_not_exists)), lift_state(post));
-        sandwich_leads_to_by_or_temp(spec, lift_state(|s: Self| s.stable_resources().contains(key)), lift_state(post), lift_state(key_not_exists));
-        leads_to_trans_temp(spec, lift_state(key_exists), lift_state(key_not_exists_or_stable), lift_state(post));
+        leads_to_framed_by_or(spec, lift_state(|s: Self| s.stable_resources().contains(key)), lift_state(post), lift_state(key_not_exists));
+        leads_to_trans(spec, lift_state(key_exists), lift_state(key_not_exists_or_stable), lift_state(post));
     });
     temp_pred_equality(lift_state(key_exists).or(lift_state(key_not_exists)), true_pred());
     temp_pred_equality(lift_state(post).or(lift_state(key_not_exists)), lift_state(post));
-    sandwich_leads_to_by_or_temp(spec, lift_state(key_exists), lift_state(post), lift_state(key_not_exists));
+    leads_to_framed_by_or(spec, lift_state(key_exists), lift_state(post), lift_state(key_not_exists));
 }
 
 proof fn lemma_pending_update_status_req_num_is_n_leads_to_daemon_set_not_exist_or_updated_or_no_more_pending_req(spec: TempPred<Self>, key: ObjectRef, make_fn: spec_fn() -> DaemonSetView, msg_num: nat)
@@ -225,7 +225,7 @@ proof fn lemma_pending_update_status_req_num_is_n_leads_to_daemon_set_not_exist_
                 }
             }
         });
-        valid_implies_implies_leads_to(spec, lift_state(pre), lift_state(post));
+        entails_implies_leads_to(spec, lift_state(pre), lift_state(post));
     } else {
         let pre_concrete_msg = |msg: MsgType<E>| lift_state(|s: Self| {
             &&& s.in_flight().filter(update_status_msg_from_bc_for(key)).len() == msg_num
diff --git a/src/kubernetes_cluster/proof/external_api_liveness.rs b/src/kubernetes_cluster/proof/external_api_liveness.rs
index 70bb9214c..72e19ec10 100644
--- a/src/kubernetes_cluster/proof/external_api_liveness.rs
+++ b/src/kubernetes_cluster/proof/external_api_liveness.rs
@@ -32,7 +32,7 @@ pub proof fn lemma_pre_leads_to_post_by_external_api(
 {
     use_tla_forall::<Self, Option<MsgType<E>>>(spec, |i| Self::external_api_next().weak_fairness(i), input);
     Self::external_api_action_pre_implies_next_pre(action, input);
-    valid_implies_trans::<Self>(
+    entails_trans::<Self>(
         lift_state(pre),
         lift_state(Self::external_api_action_pre(action, input)),
         lift_state(Self::external_api_next().pre(input))
diff --git a/src/kubernetes_cluster/proof/stateful_set_controller.rs b/src/kubernetes_cluster/proof/stateful_set_controller.rs
index 30a9d5923..a9e60055b 100644
--- a/src/kubernetes_cluster/proof/stateful_set_controller.rs
+++ b/src/kubernetes_cluster/proof/stateful_set_controller.rs
@@ -184,7 +184,7 @@ pub proof fn lemma_true_leads_to_always_stateful_set_not_exist_or_updated_or_no_
         }
     }
 
-    leads_to_stable_temp(spec, lift_action(stronger_next), true_pred(), lift_state(post));
+    leads_to_stable(spec, lift_action(stronger_next), true_pred(), lift_state(post));
 }
 
 proof fn lemma_true_leads_to_stateful_set_not_exist_or_updated_or_no_more_pending_req(spec: TempPred<Self>, key: ObjectRef, cm_key: ObjectRef, make_fn: spec_fn(rv: StringView) -> StatefulSetView)
@@ -236,12 +236,12 @@ proof fn lemma_true_leads_to_stateful_set_not_exist_or_updated_or_no_more_pendin
         });
         temp_pred_equality(lift_state(|s: Self| s.stable_resources().contains(key)).or(lift_state(key_not_exists)), lift_state(key_not_exists_or_stable));
         temp_pred_equality(lift_state(post).or(lift_state(key_not_exists)), lift_state(post));
-        sandwich_leads_to_by_or_temp(spec, lift_state(|s: Self| s.stable_resources().contains(key)), lift_state(post), lift_state(key_not_exists));
-        leads_to_trans_temp(spec, lift_state(key_exists), lift_state(key_not_exists_or_stable), lift_state(post));
+        leads_to_framed_by_or(spec, lift_state(|s: Self| s.stable_resources().contains(key)), lift_state(post), lift_state(key_not_exists));
+        leads_to_trans(spec, lift_state(key_exists), lift_state(key_not_exists_or_stable), lift_state(post));
     });
     temp_pred_equality(lift_state(key_exists).or(lift_state(key_not_exists)), true_pred());
     temp_pred_equality(lift_state(post).or(lift_state(key_not_exists)), lift_state(post));
-    sandwich_leads_to_by_or_temp(spec, lift_state(key_exists), lift_state(post), lift_state(key_not_exists));
+    leads_to_framed_by_or(spec, lift_state(key_exists), lift_state(post), lift_state(key_not_exists));
 }
 
 proof fn lemma_pending_update_status_req_num_is_n_leads_to_stateful_set_not_exist_or_updated_or_no_more_pending_req(
@@ -276,7 +276,7 @@ proof fn lemma_pending_update_status_req_num_is_n_leads_to_stateful_set_not_exis
                 }
             }
         });
-        valid_implies_implies_leads_to(spec, lift_state(pre), lift_state(post));
+        entails_implies_leads_to(spec, lift_state(pre), lift_state(post));
     } else {
         let pre_concrete_msg = |msg: MsgType<E>| lift_state(|s: Self| {
             &&& s.in_flight().filter(update_status_msg_from_bc_for(key)).len() == msg_num
diff --git a/src/kubernetes_cluster/proof/validation_rule.rs b/src/kubernetes_cluster/proof/validation_rule.rs
index 09ada659b..7c11fe834 100644
--- a/src/kubernetes_cluster/proof/validation_rule.rs
+++ b/src/kubernetes_cluster/proof/validation_rule.rs
@@ -269,8 +269,8 @@ proof fn lemma_always_triggering_cr_is_in_correct_order(spec: TempPred<Self>, cr
         }
     }
     init_invariant(spec, Self::init(), next, inv);
-    always_weaken_temp(spec, lift_state(inv), lift_state(Self::transition_rule_applies_to_etcd_and_triggering_cr(cr)));
-    always_weaken_temp(spec, lift_state(inv), lift_state(Self::transition_rule_applies_to_scheduled_and_triggering_cr(cr)));
+    always_weaken(spec, lift_state(inv), lift_state(Self::transition_rule_applies_to_etcd_and_triggering_cr(cr)));
+    always_weaken(spec, lift_state(inv), lift_state(Self::transition_rule_applies_to_scheduled_and_triggering_cr(cr)));
 }
 
 }
diff --git a/src/state_machine/action.rs b/src/state_machine/action.rs
index 5d14490a3..1a67b380d 100644
--- a/src/state_machine/action.rs
+++ b/src/state_machine/action.rs
@@ -46,26 +46,10 @@ impl<State, Input, Output> Action<State, Input, Output> {
             spec.entails(self.weak_fairness(input)),
         ensures spec.entails(lift_state(pre).leads_to(lift_state(post))),
     {
-        always_implies_preserved_by_always_temp::<State>(spec, lift_state(pre), lift_state(self.pre(input)));
-        leads_to_weaken_temp::<State>(spec, always(lift_state(self.pre(input))), lift_action(self.forward(input)), always(lift_state(pre)), lift_action(self.forward(input)));
+        always_implies_preserved_by_always::<State>(spec, lift_state(pre), lift_state(self.pre(input)));
+        leads_to_weaken::<State>(spec, always(lift_state(self.pre(input))), lift_action(self.forward(input)), always(lift_state(pre)), lift_action(self.forward(input)));
         wf1_variant_temp::<State>(spec, lift_action(next), lift_action(self.forward(input)), lift_state(pre), lift_state(post));
     }
-
-    /// `wf1_borrow_from_spec` is a specialized version of temporal_logic_rules::wf1 for Action
-    pub proof fn wf1_borrow_from_spec(self, input: Input, spec: TempPred<State>, next: ActionPred<State>, c: StatePred<State>, pre: StatePred<State>, post: StatePred<State>)
-        requires
-            forall |s, s_prime: State| pre(s) && c(s) && #[trigger] next(s, s_prime) ==> pre(s_prime) || post(s_prime),
-            forall |s, s_prime: State| pre(s) && c(s) && #[trigger] next(s, s_prime) && self.forward(input)(s, s_prime) ==> post(s_prime),
-            spec.entails(always(lift_action(next))),
-            spec.entails(always((lift_state(pre).and(lift_state(c))).implies(lift_state(self.pre(input))))),
-            spec.entails(self.weak_fairness(input)),
-            spec.entails(always(lift_state(c))),
-        ensures spec.entails(lift_state(pre).leads_to(lift_state(post))),
-    {
-        always_implies_preserved_by_always_temp::<State>(spec, lift_state(pre).and(lift_state(c)), lift_state(self.pre(input)));
-        leads_to_weaken_temp::<State>(spec, always(lift_state(self.pre(input))), lift_action(self.forward(input)), always(lift_state(pre).and(lift_state(c))), lift_action(self.forward(input)));
-        wf1_variant_borrow_from_spec_temp::<State>(spec, lift_action(next), lift_action(self.forward(input)), lift_state(c), lift_state(pre), lift_state(post));
-    }
 }
 
 #[is_variant]
diff --git a/src/temporal_logic/defs.rs b/src/temporal_logic/defs.rs
index ff8e9fdfe..dfbf7a2af 100644
--- a/src/temporal_logic/defs.rs
+++ b/src/temporal_logic/defs.rs
@@ -63,11 +63,6 @@ impl<T> TempPred<T> {
         TempPred::new(|ex: Execution<T>| self.satisfied_by(ex) ==> other.satisfied_by(ex))
     }
 
-    /// `<=>` for temporal predicates in TLA+ (i.e., `<==>` in Verus).
-    pub open spec fn equals(self, other: Self) -> Self {
-        TempPred::new(|ex: Execution<T>| self.satisfied_by(ex) <==> other.satisfied_by(ex))
-    }
-
     /// `~>` for temporal predicates in TLA+.
     /// Returns a temporal predicate that is satisfied
     /// iff it is always the case that `self` getting satisfied implies `other` eventually getting satisfied.
@@ -178,7 +173,7 @@ pub open spec fn true_pred<T>() -> TempPred<T> {
 }
 
 pub open spec fn false_pred<T>() -> TempPred<T> {
-    lift_state(|s: T| false)
+    not(true_pred())
 }
 
 }
diff --git a/src/temporal_logic/rules.rs b/src/temporal_logic/rules.rs
index c96f6ba08..26eb160b2 100644
--- a/src/temporal_logic/rules.rs
+++ b/src/temporal_logic/rules.rs
@@ -97,13 +97,6 @@ proof fn implies_contraposition_apply<T>(ex: Execution<T>, p: TempPred<T>, q: Te
     ensures not(p).satisfied_by(ex),
 {}
 
-proof fn equals_apply<T>(ex: Execution<T>, p: TempPred<T>, q: TempPred<T>)
-    requires
-        p.equals(q).satisfied_by(ex),
-        p.satisfied_by(ex),
-    ensures q.satisfied_by(ex),
-{}
-
 proof fn implies_apply_with_always<T>(ex: Execution<T>, p: TempPred<T>, q: TempPred<T>)
     requires
         always(p.implies(q)).satisfied_by(ex),
@@ -123,15 +116,6 @@ proof fn entails_apply<T>(ex: Execution<T>, p: TempPred<T>, q: TempPred<T>)
     implies_apply::<T>(ex, p, q);
 }
 
-proof fn entails_apply_auto<T>()
-    ensures forall |ex: Execution<T>, p: TempPred<T>, q: TempPred<T>| #[trigger] p.entails(q) && p.satisfied_by(ex) ==> #[trigger] q.satisfied_by(ex),
-{
-    assert forall |ex: Execution<T>, p: TempPred<T>, q: TempPred<T>|
-    #[trigger] valid(p.implies(q)) && p.satisfied_by(ex) implies #[trigger] q.satisfied_by(ex) by {
-        entails_apply(ex, p, q);
-    };
-}
-
 proof fn not_proved_by_contraposition<T>(ex: Execution<T>, p: TempPred<T>, q: TempPred<T>)
     requires
         p.implies(q).satisfied_by(ex),
@@ -202,56 +186,6 @@ spec fn eventually_choose_witness<T>(ex: Execution<T>, p: TempPred<T>) -> nat
     witness
 }
 
-proof fn equals_trans<T>(ex: Execution<T>, p: TempPred<T>, q: TempPred<T>, r: TempPred<T>)
-    requires
-        p.equals(q).satisfied_by(ex),
-        q.equals(r).satisfied_by(ex),
-    ensures p.equals(r).satisfied_by(ex),
-{}
-
-proof fn implies_trans<T>(ex: Execution<T>, p: TempPred<T>, q: TempPred<T>, r: TempPred<T>)
-    requires
-        p.implies(q).satisfied_by(ex),
-        q.implies(r).satisfied_by(ex),
-    ensures p.implies(r).satisfied_by(ex),
-{}
-
-proof fn equals_to_implies<T>(ex: Execution<T>, p: TempPred<T>, q: TempPred<T>)
-    requires p.equals(q).satisfied_by(ex),
-    ensures
-        p.implies(q).satisfied_by(ex),
-        q.implies(p).satisfied_by(ex),
-{}
-
-proof fn implies_to_equals<T>(ex: Execution<T>, p: TempPred<T>, q: TempPred<T>)
-    requires
-        p.implies(q).satisfied_by(ex),
-        q.implies(p).satisfied_by(ex),
-    ensures p.equals(q).satisfied_by(ex),
-{}
-
-proof fn valid_equals_to_valid_implies<T>(p: TempPred<T>, q: TempPred<T>)
-    requires valid(p.equals(q)),
-    ensures
-        valid(p.implies(q)),
-        valid(q.implies(p)),
-{
-    assert forall |ex| p.implies(q).satisfied_by(ex) && q.implies(p).satisfied_by(ex) by {
-        equals_to_implies::<T>(ex, p, q);
-    };
-}
-
-proof fn valid_implies_to_valid_equals<T>(p: TempPred<T>, q: TempPred<T>)
-    requires
-        valid(p.implies(q)),
-        valid(q.implies(p)),
-    ensures valid(p.equals(q)),
-{
-    assert forall |ex| p.equals(q).satisfied_by(ex) by {
-        implies_to_equals(ex, p, q);
-    };
-}
-
 proof fn valid_p_implies_always_p<T>(p: TempPred<T>)
     requires valid(p),
     ensures valid(always(p)),
@@ -261,27 +195,6 @@ proof fn valid_p_implies_always_p<T>(p: TempPred<T>)
     };
 }
 
-proof fn implies_and<T>(p: TempPred<T>, q: TempPred<T>, r: TempPred<T>)
-    requires
-        valid(p.implies(q)),
-        valid(p.implies(r)),
-    ensures valid(p.implies(q.and(r))),
-{
-    assert forall |ex| p.satisfied_by(ex) implies #[trigger] q.and(r).satisfied_by(ex) by {
-        implies_apply::<T>(ex, p, q);
-        implies_apply::<T>(ex, p, r);
-    };
-}
-
-proof fn always_implies_current<T>(p: TempPred<T>)
-    ensures valid(always(p).implies(p)),
-{
-    assert forall |ex| always(p).satisfied_by(ex) implies #[trigger] p.satisfied_by(ex) by {
-        always_unfold(ex, p);
-        execution_equality::<T>(ex, ex.suffix(0));
-    };
-}
-
 proof fn always_distributed_by_and<T>(p: TempPred<T>, q: TempPred<T>)
     ensures valid(always(p.and(q)).implies(always(p).and(always(q)))),
 {
@@ -372,59 +285,6 @@ proof fn next_preserves_inv_rec<T>(ex: Execution<T>, next: TempPred<T>, inv: Tem
     }
 }
 
-proof fn p_is_preserved_before_t<T>(ex: Execution<T>, next: TempPred<T>, p: TempPred<T>, q: TempPred<T>, t: nat, i: nat)
-    requires
-        i <= t,
-        p.satisfied_by(ex),
-        forall |idx: nat| next.satisfied_by(#[trigger] ex.suffix(idx)),
-        forall |idx: nat| idx < t ==> !q.satisfied_by(#[trigger] ex.suffix(idx)),
-        forall |idx: nat| p.satisfied_by(ex.suffix(idx)) && !q.satisfied_by(ex.suffix(idx)) && next.satisfied_by(#[trigger] ex.suffix(idx))
-            ==> p.satisfied_by(ex.suffix(idx + 1)),
-    ensures p.satisfied_by(ex.suffix(i)),
-    decreases i,
-{
-    if i == 0 {
-        execution_equality::<T>(ex, ex.suffix(0));
-    } else {
-        p_is_preserved_before_t::<T>(ex, next, p, q, t, (i-1) as nat);
-    }
-}
-
-proof fn confluence_at_some_point<T>(ex: Execution<T>, next: TempPred<T>, p: TempPred<T>, q: TempPred<T>, i: nat)
-    requires
-        p.satisfied_by(ex),
-        q.satisfied_by(ex.suffix(i)),
-        always(p.and(not(q)).and(next).implies(later(p))).satisfied_by(ex),
-        always(next).satisfied_by(ex),
-    ensures exists |idx: nat| p.and(q).satisfied_by(#[trigger] ex.suffix(idx)),
-    decreases i,
-{
-    if i == 0 {
-        execution_equality::<T>(ex, ex.suffix(0));
-        assert(p.and(q).satisfied_by(ex.suffix(0)));
-    } else {
-        if exists |j: nat| {
-            &&& j < i
-            &&& q.satisfied_by(#[trigger] ex.suffix(j))
-        } {
-            let t = choose |j: nat| {
-                &&& j < i
-                &&& q.satisfied_by(#[trigger] ex.suffix(j))
-            };
-            confluence_at_some_point::<T>(ex, next, p, q, t);
-        } else {
-            assert forall |idx: nat| p.satisfied_by(ex.suffix(idx)) && !q.satisfied_by(ex.suffix(idx)) && next.satisfied_by(#[trigger] ex.suffix(idx))
-            implies p.satisfied_by(ex.suffix(idx + 1)) by {
-                always_unfold::<T>(ex, p.and(not(q)).and(next).implies(later(p)));
-                implies_apply::<T>(ex.suffix(idx), p.and(not(q)).and(next), later(p));
-                execution_equality::<T>(ex.suffix(idx).suffix(1), ex.suffix(idx + 1));
-            };
-            p_is_preserved_before_t::<T>(ex, next, p, q, i, i);
-            assert(p.and(q).satisfied_by(ex.suffix(i)));
-        }
-    }
-}
-
 proof fn instantiate_entailed_always<T>(ex: Execution<T>, i: nat, spec: TempPred<T>, p: TempPred<T>)
     requires
         spec.satisfied_by(ex),
@@ -448,7 +308,7 @@ proof fn instantiate_entailed_leads_to<T>(ex: Execution<T>, i: nat, spec: TempPr
 /// All the lemmas above are used internally for proving the lemmas below
 /// The following lemmas are used by developers to simplify liveness/safety proof
 
-pub proof fn implies_to_leads_to<T>(spec: TempPred<T>, p: TempPred<T>, q: TempPred<T>)
+pub proof fn always_implies_to_leads_to<T>(spec: TempPred<T>, p: TempPred<T>, q: TempPred<T>)
     requires spec.entails(always(p.implies(q))),
     ensures spec.entails(p.leads_to(q)),
 {
@@ -472,11 +332,12 @@ pub proof fn execution_equality<T>(ex1: Execution<T>, ex2: Execution<T>)
 }
 
 pub proof fn temp_pred_equality<T>(p: TempPred<T>, q: TempPred<T>)
-    requires valid(p.equals(q)),
+    requires
+        p.entails(q),
+        q.entails(p),
     ensures p == q,
 {
     assert forall |ex: Execution<T>| #[trigger] (p.pred)(ex) == (q.pred)(ex) by {
-        valid_equals_to_valid_implies::<T>(p, q);
         if (p.pred)(ex) {
             implies_apply::<T>(ex, p, q);
         } else {
@@ -496,7 +357,7 @@ pub proof fn always_to_always_later<T>(spec: TempPred<T>, p: TempPred<T>)
             execution_equality(ex.suffix(i).suffix(1), ex.suffix(1).suffix(i));
         }
     }
-    valid_implies_trans(spec, always(p), always(later(p)));
+    entails_trans(spec, always(p), always(later(p)));
 }
 
 proof fn always_double_equality<T>(p: TempPred<T>)
@@ -564,7 +425,7 @@ proof fn p_and_always_p_equals_always_p<T>(p: TempPred<T>)
 }
 
 proof fn a_to_temp_pred_equality<T, A>(p: spec_fn(A) -> TempPred<T>, q: spec_fn(A) -> TempPred<T>)
-    requires forall |a: A| #[trigger] valid(p(a).equals(q(a))),
+    requires forall |a: A| #[trigger] p(a).entails(q(a)) && q(a).entails(p(a)),
     ensures p == q,
 {
     assert forall |a: A| #[trigger] p(a) == q(a) by {
@@ -624,7 +485,7 @@ pub proof fn tla_forall_always_equality<T, A>(a_to_p: spec_fn(A) -> TempPred<T>)
 }
 
 pub proof fn tla_forall_always_equality_variant<T, A>(a_to_always: spec_fn(A) -> TempPred<T>, a_to_p: spec_fn(A) -> TempPred<T>)
-    requires forall |a: A| #![trigger a_to_always(a)] valid(a_to_always(a).equals((|a: A| always(a_to_p(a)))(a))),
+    requires forall |a: A| #![trigger a_to_always(a)] a_to_always(a).entails((|a: A| always(a_to_p(a)))(a)) && ((|a: A| always(a_to_p(a)))(a)).entails(a_to_always(a)),
     ensures tla_forall(a_to_always) == always(tla_forall(a_to_p)),
 {
     a_to_temp_pred_equality::<T, A>(a_to_always, |a: A| always(a_to_p(a)));
@@ -679,8 +540,8 @@ pub proof fn always_tla_forall_apply<T, A>(spec: TempPred<T>, a_to_p: spec_fn(A)
     requires spec.entails(always(tla_forall(a_to_p))),
     ensures spec.entails(always(a_to_p(a))),
 {
-    implies_preserved_by_always_temp(tla_forall(a_to_p), a_to_p(a));
-    valid_implies_trans(spec, always(tla_forall(a_to_p)), always(a_to_p(a)));
+    entails_preserved_by_always(tla_forall(a_to_p), a_to_p(a));
+    entails_trans(spec, always(tla_forall(a_to_p)), always(a_to_p(a)));
 }
 
 proof fn tla_forall_or_equality<T, A>(a_to_p: spec_fn(A) -> TempPred<T>, q: TempPred<T>)
@@ -793,7 +654,7 @@ pub proof fn spec_entails_tla_forall<T, A>(spec: TempPred<T>, a_to_p: spec_fn(A)
     };
 }
 
-proof fn always_implies_forall_intro<T, A>(spec: TempPred<T>, p: TempPred<T>, a_to_q: spec_fn(A) -> TempPred<T>)
+pub proof fn always_implies_forall_intro<T, A>(spec: TempPred<T>, p: TempPred<T>, a_to_q: spec_fn(A) -> TempPred<T>)
     requires forall |a: A| #[trigger] spec.entails(always(p.implies(a_to_q(a)))),
     ensures spec.entails(always(p.implies(tla_forall(a_to_q)))),
 {
@@ -822,8 +683,8 @@ pub proof fn use_tla_forall<T, A>(spec: TempPred<T>, a_to_p: spec_fn(A) -> TempP
     requires spec.entails(tla_forall(a_to_p)),
     ensures spec.entails(a_to_p(a)),
 {
-    entails_apply_auto::<T>();
-    assert forall |ex: Execution<T>| #[trigger] spec.implies(a_to_p(a)).satisfied_by(ex) by {
+    assert forall |ex: Execution<T>| #[trigger] spec.satisfied_by(ex) implies (a_to_p(a)).satisfied_by(ex) by {
+        entails_apply(ex, spec, tla_forall(a_to_p));
         assert(spec.implies(tla_forall(a_to_p)).satisfied_by(ex));
     };
 }
@@ -857,26 +718,6 @@ pub proof fn eliminate_always<T>(spec: TempPred<T>, p: TempPred<T>)
     }
 }
 
-proof fn stable_spec_entails_always_p<T>(spec: TempPred<T>, p: TempPred<T>)
-    requires
-        valid(stable(spec)),
-        spec.entails(p),
-    ensures spec.entails(always(p)),
-{
-    assert_by(
-        spec.entails(always(spec)),
-        {
-            assert forall |ex| #[trigger] spec.implies(always(spec)).satisfied_by(ex) by {
-                assert(valid(stable(spec)));
-                assert(stable(spec).satisfied_by(ex));
-                stable_unfold::<T>(ex, spec);
-            }
-        }
-    );
-    implies_preserved_by_always_temp(spec, p);
-    valid_implies_trans(spec, always(spec), always(p));
-}
-
 /// Entails p and q if entails each of them.
 /// pre:
 ///     spec |= p
@@ -1038,8 +879,8 @@ macro_rules! combine_spec_entails_always_n_internal {
                 entails_always_and_n!($spec, $($tail)*);
             }
         );
-        implies_preserved_by_always_temp(combine_with_next!($($tail)*), $partial_spec);
-        valid_implies_trans($spec, always(combine_with_next!($($tail)*)), always($partial_spec));
+        entails_preserved_by_always(combine_with_next!($($tail)*), $partial_spec);
+        entails_trans($spec, always(combine_with_next!($($tail)*)), always($partial_spec));
     };
 }
 
@@ -1074,10 +915,10 @@ macro_rules! invariant_n_internal {
                 entails_always_and_n!($spec, $($tail)*);
             }
         );
-        implies_preserved_by_always_temp(combine_with_next!($($tail)*), $partial_spec);
-        valid_implies_trans($spec, always(combine_with_next!($($tail)*)), always($partial_spec));
-        implies_preserved_by_always_temp($partial_spec, $inv);
-        valid_implies_trans($spec, always($partial_spec), always($inv));
+        entails_preserved_by_always(combine_with_next!($($tail)*), $partial_spec);
+        entails_trans($spec, always(combine_with_next!($($tail)*)), always($partial_spec));
+        entails_preserved_by_always($partial_spec, $inv);
+        entails_trans($spec, always($partial_spec), always($inv));
     };
 }
 
@@ -1221,21 +1062,6 @@ pub proof fn unpack_conditions_from_spec<T>(spec: TempPred<T>, c: TempPred<T>, p
     };
 }
 
-proof fn borrow_conditions_from_spec<T>(spec: TempPred<T>, c: TempPred<T>, p: TempPred<T>, q: TempPred<T>)
-    requires
-        spec.entails(p.and(c).leads_to(q)),
-        spec.entails(always(c)),
-    ensures spec.entails(p.leads_to(q)),
-{
-    assert forall |ex| #[trigger] spec.satisfied_by(ex) implies p.leads_to(q).satisfied_by(ex) by {
-        assert forall |i| #[trigger] p.satisfied_by(ex.suffix(i)) implies eventually(q).satisfied_by(ex.suffix(i)) by {
-            implies_apply(ex, spec, always(c));
-            implies_apply(ex, spec, p.and(c).leads_to(q));
-            implies_apply(ex.suffix(i), p.and(c), eventually(q));
-        }
-    }
-}
-
 /// Pack the conditions from the right to the left side of |=
 /// pre:
 ///     spec |= p /\ c ~> q
@@ -1258,15 +1084,19 @@ proof fn pack_conditions_to_spec<T>(spec: TempPred<T>, c: TempPred<T>, p: TempPr
 /// This lemma is used to make the predicate as concise as possible.
 /// Similar to the first-order logic where p equals p /\ q when p -> q is satisfied,
 /// we can reduce the size of predicate when some part of it implies the rest.
-pub proof fn simplify_predicate<T>(simpler: TempPred<T>, redundant: TempPred<T>)
-    requires simpler.entails(redundant),
-    ensures simpler == simpler.and(redundant),
+/// pre:
+///     p |= q
+/// post:
+///     p == p /\ q
+pub proof fn simplify_predicate<T>(p: TempPred<T>, q: TempPred<T>)
+    requires p.entails(q),
+    ensures p == p.and(q),
 {
-    assert forall |ex| #[trigger] simpler.satisfied_by(ex) implies simpler.and(redundant).satisfied_by(ex) by {
-        entails_and_temp::<T>(simpler, simpler, redundant);
-        entails_apply::<T>(ex, simpler, simpler.and(redundant));
+    assert forall |ex| #[trigger] p.satisfied_by(ex) implies p.and(q).satisfied_by(ex) by {
+        entails_and_temp::<T>(p, p, q);
+        entails_apply::<T>(ex, p, p.and(q));
     };
-    temp_pred_equality::<T>(simpler, simpler.and(redundant));
+    temp_pred_equality::<T>(p, p.and(q));
 }
 
 /// Prove safety by induction.
@@ -1306,7 +1136,8 @@ pub proof fn strengthen_next<T>(spec: TempPred<T>, next: ActionPred<T>, inv: Sta
     requires
         spec.entails(always(lift_action(next))),
         spec.entails(always(lift_state(inv))),
-        valid(lift_action(next_and_inv).equals(lift_action(next).and(lift_state(inv)))),
+        lift_action(next_and_inv).entails(lift_action(next).and(lift_state(inv))),
+        lift_action(next).and(lift_state(inv)).entails(lift_action(next_and_inv)),
     ensures spec.entails(always(lift_action(next_and_inv))),
 {
     entails_and_temp::<T>(spec, always(lift_action(next)), always(lift_state(inv)));
@@ -1356,33 +1187,6 @@ pub proof fn wf1_variant_temp<T>(spec: TempPred<T>, next: TempPred<T>, forward:
     }
 }
 
-pub proof fn wf1_variant_borrow_from_spec_temp<T>(spec: TempPred<T>, next: TempPred<T>, forward: TempPred<T>, c: TempPred<T>, p: TempPred<T>, q: TempPred<T>)
-    requires
-        spec.entails(always(p.and(c).and(next).implies(later(p).or(later(q))))),
-        spec.entails(always(p.and(c).and(next).and(forward).implies(later(q)))),
-        spec.entails(always(next)),
-        spec.entails(always(p.and(c)).leads_to(forward)),
-        spec.entails(always(c)),
-    ensures spec.entails(p.leads_to(q)),
-{
-    assert forall |ex| #[trigger] spec.satisfied_by(ex)
-    implies always(p.and(c).and(next).implies(later(p.and(c)).or(later(q)))).satisfied_by(ex) by {
-        implies_apply::<T>(ex, spec, always(p.and(c).and(next).implies(later(p).or(later(q)))));
-        implies_apply::<T>(ex, spec, always(c));
-        always_unfold(ex, p.and(c).and(next).implies(later(p).or(later(q))));
-        always_unfold(ex, c);
-        assert forall |i| #[trigger] p.and(c).and(next).satisfied_by(ex.suffix(i))
-        implies later(p.and(c)).or(later(q)).satisfied_by(ex.suffix(i)) by {
-            implies_apply(ex.suffix(i), p.and(c).and(next), later(p).or(later(q)));
-            execution_equality(ex.suffix(i).suffix(1), ex.suffix(i + 1));
-            temp_pred_equality(later(p.and(c)), later(p).and(later(c)));
-        }
-    }
-
-    wf1_variant_temp(spec, next, forward, p.and(c), q);
-    borrow_conditions_from_spec(spec, c, p, q);
-}
-
 /// Get the initial leads_to with a stronger wf assumption than wf1_variant.
 /// pre:
 ///     |= p /\ next => p' \/ q'
@@ -1421,7 +1225,7 @@ pub proof fn wf1<T>(spec: TempPred<T>, next: ActionPred<T>, forward: ActionPred<
 ///     q |= r
 /// post:
 ///     p |= r
-pub proof fn valid_implies_trans<T>(p: TempPred<T>, q: TempPred<T>, r: TempPred<T>)
+pub proof fn entails_trans<T>(p: TempPred<T>, q: TempPred<T>, r: TempPred<T>)
     requires
         p.entails(q),
         q.entails(r),
@@ -1435,26 +1239,26 @@ pub proof fn valid_implies_trans<T>(p: TempPred<T>, q: TempPred<T>, r: TempPred<
 
 /// If p implies q for all executions, p will leads to q anyway.
 /// pre:
-///     |= p => q
+///     p |= q
 /// post:
 ///     spec |= p ~> q
 /// Note: there is no constraint on spec, it can be true_pred().
-pub proof fn valid_implies_implies_leads_to<T>(spec: TempPred<T>, p: TempPred<T>, q: TempPred<T>)
-    requires valid(p.implies(q)),
+pub proof fn entails_implies_leads_to<T>(spec: TempPred<T>, p: TempPred<T>, q: TempPred<T>)
+    requires p.entails(q),
     ensures spec.entails(p.leads_to(q)),
 {
     valid_p_implies_always_p(p.implies(q));
-    implies_to_leads_to(spec, p, q);
+    always_implies_to_leads_to(spec, p, q);
 }
 
 /// Introduce always to both sides of implies.
 /// pre:
-///     |= p => q
+///     p |= q
 /// post:
-///     |= []p => []q
-pub proof fn implies_preserved_by_always_temp<T>(p: TempPred<T>, q: TempPred<T>)
-    requires valid(p.implies(q)),
-    ensures valid(always(p).implies(always(q))),
+///     []p |= []q
+pub proof fn entails_preserved_by_always<T>(p: TempPred<T>, q: TempPred<T>)
+    requires p.entails(q),
+    ensures always(p).entails(always(q)),
 {
     assert forall |ex| always(p).satisfied_by(ex) implies always(q).satisfied_by(ex) by {
         assert forall |i:nat| q.satisfied_by(#[trigger] ex.suffix(i)) by {
@@ -1470,13 +1274,13 @@ pub proof fn implies_preserved_by_always_temp<T>(p: TempPred<T>, q: TempPred<T>)
 ///     spec |= []p
 /// post:
 ///     spec |= []q
-pub proof fn always_weaken_temp<T>(spec: TempPred<T>, p: TempPred<T>, q: TempPred<T>)
+pub proof fn always_weaken<T>(spec: TempPred<T>, p: TempPred<T>, q: TempPred<T>)
     requires
         valid(p.implies(q)),
         spec.entails(always(p)),
     ensures spec.entails(always(q)),
 {
-    implies_preserved_by_always_temp::<T>(p, q);
+    entails_preserved_by_always::<T>(p, q);
     assert forall |ex| #[trigger] spec.satisfied_by(ex) implies always(q).satisfied_by(ex) by {
         implies_apply::<T>(ex, spec, always(p));
         implies_apply::<T>(ex, always(p), always(q));
@@ -1488,7 +1292,7 @@ pub proof fn always_weaken_temp<T>(spec: TempPred<T>, p: TempPred<T>, q: TempPre
 ///     spec |= [](p => q)
 /// post:
 ///     spec |= []([]p => []q)
-pub proof fn always_implies_preserved_by_always_temp<T>(spec: TempPred<T>, p: TempPred<T>, q: TempPred<T>)
+pub proof fn always_implies_preserved_by_always<T>(spec: TempPred<T>, p: TempPred<T>, q: TempPred<T>)
     requires spec.entails(always(p.implies(q))),
     ensures spec.entails(always(always(p).implies(always(q)))),
 {
@@ -1507,6 +1311,13 @@ pub proof fn always_implies_preserved_by_always_temp<T>(spec: TempPred<T>, p: Te
     };
 }
 
+/// Enhance the conclusion of leads to always using invariant.
+/// pre:
+///     spec |= []inv
+///     spec |= p ~> []q1
+///     q1 /\ inv |= q2
+/// post:
+///     spec |= p ~> []q2
 pub proof fn leads_to_always_enhance<T>(spec: TempPred<T>, inv: TempPred<T>, p: TempPred<T>, q1: TempPred<T>, q2: TempPred<T>)
     requires
         spec.entails(always(inv)),
@@ -1537,7 +1348,7 @@ pub proof fn leads_to_always_enhance<T>(spec: TempPred<T>, inv: TempPred<T>, p:
 ///     spec |= p ~> q
 /// post:
 ///     spec |= <>q
-pub proof fn leads_to_apply_temp<T>(spec: TempPred<T>, p: TempPred<T>, q: TempPred<T>)
+pub proof fn leads_to_apply<T>(spec: TempPred<T>, p: TempPred<T>, q: TempPred<T>)
     requires
         spec.entails(p),
         spec.entails(p.leads_to(q)),
@@ -1558,7 +1369,7 @@ pub proof fn leads_to_apply_temp<T>(spec: TempPred<T>, p: TempPred<T>, q: TempPr
 ///     spec |= q ~> r
 /// post:
 ///     spec |= p ~> r
-pub proof fn leads_to_trans_temp<T>(spec: TempPred<T>, p: TempPred<T>, q: TempPred<T>, r: TempPred<T>)
+pub proof fn leads_to_trans<T>(spec: TempPred<T>, p: TempPred<T>, q: TempPred<T>, r: TempPred<T>)
     requires
         spec.entails(p.leads_to(q)),
         spec.entails(q.leads_to(r)),
@@ -1595,10 +1406,10 @@ macro_rules! leads_to_trans_n {
 #[macro_export]
 macro_rules! leads_to_trans_n_internal {
     ($spec:expr, $p1:expr, $p2:expr, $p3:expr) => {
-        leads_to_trans_temp($spec, $p1, $p2, $p3);
+        leads_to_trans($spec, $p1, $p2, $p3);
     };
     ($spec:expr, $p1:expr, $p2:expr, $p3:expr, $($tail:tt)*) => {
-        leads_to_trans_temp($spec, $p1, $p2, $p3);
+        leads_to_trans($spec, $p1, $p2, $p3);
         leads_to_trans_n_internal!($spec, $p1, $p3, $($tail)*);
     };
 }
@@ -1613,17 +1424,17 @@ pub use leads_to_trans_n_internal;
 ///     spec |= p1 ~> q1
 /// post:
 ///     spec |= p2 ~> q2
-pub proof fn leads_to_weaken_temp<T>(spec: TempPred<T>, p1: TempPred<T>, q1: TempPred<T>, p2: TempPred<T>, q2: TempPred<T>)
+pub proof fn leads_to_weaken<T>(spec: TempPred<T>, p1: TempPred<T>, q1: TempPred<T>, p2: TempPred<T>, q2: TempPred<T>)
     requires
         spec.entails(always(p2.implies(p1))),
         spec.entails(always(q1.implies(q2))),
         spec.entails(p1.leads_to(q1)),
     ensures spec.entails(p2.leads_to(q2)),
 {
-    implies_to_leads_to::<T>(spec, p2, p1);
-    implies_to_leads_to::<T>(spec, q1, q2);
-    leads_to_trans_temp::<T>(spec, p2, p1, q1);
-    leads_to_trans_temp::<T>(spec, p2, q1, q2);
+    always_implies_to_leads_to::<T>(spec, p2, p1);
+    always_implies_to_leads_to::<T>(spec, q1, q2);
+    leads_to_trans::<T>(spec, p2, p1, q1);
+    leads_to_trans::<T>(spec, p2, q1, q2);
 }
 
 /// Combine the premises of two leads_to using or.
@@ -1632,7 +1443,7 @@ pub proof fn leads_to_weaken_temp<T>(spec: TempPred<T>, p1: TempPred<T>, q1: Tem
 ///     spec |= q ~> r
 /// post:
 ///     spec |= (p \/ q) ~> r
-pub proof fn or_leads_to_combine_temp<T>(spec: TempPred<T>, p: TempPred<T>, q: TempPred<T>, r: TempPred<T>)
+pub proof fn or_leads_to_combine<T>(spec: TempPred<T>, p: TempPred<T>, q: TempPred<T>, r: TempPred<T>)
     requires
         spec.entails(p.leads_to(r)),
         spec.entails(q.leads_to(r)),
@@ -1668,10 +1479,10 @@ macro_rules! or_leads_to_combine_n {
 #[macro_export]
 macro_rules! or_leads_to_combine_n_internal {
     ($spec:expr, $p1:expr, $p2:expr; $q:expr) => {
-        or_leads_to_combine_temp($spec, $p1, $p2, $q);
+        or_leads_to_combine($spec, $p1, $p2, $q);
     };
     ($spec:expr, $p1:expr, $p2:expr, $($rest:expr),+; $q:expr) => {
-        or_leads_to_combine_temp($spec, $p1, $p2, $q);
+        or_leads_to_combine($spec, $p1, $p2, $q);
         or_leads_to_combine_n_internal!($spec, $p1.or($p2), $($rest),+; $q);
     };
 }
@@ -1714,10 +1525,10 @@ macro_rules! leads_to_always_combine_n {
 #[macro_export]
 macro_rules! leads_to_always_combine_n_internal {
     ($spec:expr, $p:expr, $q1:expr, $q2:expr) => {
-        leads_to_always_combine_temp($spec, $p, $q1, $q2);
+        leads_to_always_combine($spec, $p, $q1, $q2);
     };
     ($spec:expr, $p:expr, $q1:expr, $q2:expr, $($tail:tt)*) => {
-        leads_to_always_combine_temp($spec, $p, $q1, $q2);
+        leads_to_always_combine($spec, $p, $q1, $q2);
         always_and_equality($q1, $q2);
         leads_to_always_combine_n_internal!($spec, $p, $q1.and($q2), $($tail)*);
     };
@@ -1815,7 +1626,7 @@ pub proof fn leads_to_always_tla_forall<T, A>(spec: TempPred<T>, p: TempPred<T>,
 ///     spec |= p ~> []r
 /// post:
 ///     spec |= p ~> [](q /\ r)
-pub proof fn leads_to_always_combine_temp<T>(spec: TempPred<T>, p: TempPred<T>, q: TempPred<T>, r: TempPred<T>)
+pub proof fn leads_to_always_combine<T>(spec: TempPred<T>, p: TempPred<T>, q: TempPred<T>, r: TempPred<T>)
     requires
         spec.entails(p.leads_to(always(q))),
         spec.entails(p.leads_to(always(r))),
@@ -1848,14 +1659,14 @@ pub proof fn leads_to_always_combine_temp<T>(spec: TempPred<T>, p: TempPred<T>,
     always_and_equality(q, r);
 }
 
-/// Get leads_to always.
+/// Prove p leads_to always q by showing that q is preserved.
 /// pre:
 ///     spec |= [](q /\ next => q')
 ///     spec |= []next
 ///     spec |= p ~> q
 /// post:
 ///     spec |= p ~> []q
-pub proof fn leads_to_stable_temp<T>(spec: TempPred<T>, next: TempPred<T>, p: TempPred<T>, q: TempPred<T>)
+pub proof fn leads_to_stable<T>(spec: TempPred<T>, next: TempPred<T>, p: TempPred<T>, q: TempPred<T>)
     requires
         spec.entails(always(q.and(next).implies(later(q)))),
         spec.entails(always(next)),
@@ -1897,7 +1708,7 @@ pub proof fn leads_to_stable_temp<T>(spec: TempPred<T>, next: TempPred<T>, p: Te
 ///     spec |= p ~> q
 /// post:
 ///     spec |= p \/ r ~> q \/ r
-pub proof fn sandwich_leads_to_by_or_temp<T>(spec: TempPred<T>, p: TempPred<T>, q: TempPred<T>, r: TempPred<T>)
+pub proof fn leads_to_framed_by_or<T>(spec: TempPred<T>, p: TempPred<T>, q: TempPred<T>, r: TempPred<T>)
     requires spec.entails(p.leads_to(q)),
     ensures spec.entails(p.or(r).leads_to(q.or(r))),
 {
@@ -1930,9 +1741,9 @@ pub proof fn leads_to_shortcut_temp<T>(spec: TempPred<T>, p: TempPred<T>, q: Tem
         spec.entails(q.leads_to(r.or(s))),
     ensures spec.entails(p.leads_to(r.or(s))),
 {
-    sandwich_leads_to_by_or_temp(spec, q, r.or(s), s);
+    leads_to_framed_by_or(spec, q, r.or(s), s);
     temp_pred_equality(r.or(s).or(s), r.or(s));
-    leads_to_trans_temp(spec, p, q.or(s), r.or(s));
+    leads_to_trans(spec, p, q.or(s), r.or(s));
 }
 
 /// Concluding p(n) ~> p(0) using ranking functions, with a step of one.
@@ -2032,4 +1843,25 @@ pub proof fn vacuous_leads_to<T>(spec: TempPred<T>, p: TempPred<T>, q: TempPred<
     }
 }
 
+/// Proving p leads to q by borrowing the inv.
+/// pre:
+///     spec |= p /\ inv ~> q
+///     spec |= []inv
+/// post:
+///     spec |= p ~> q
+pub proof fn leads_to_by_borrowing_inv<T>(spec: TempPred<T>, p: TempPred<T>, q: TempPred<T>, inv: TempPred<T>)
+    requires
+        spec.entails(p.and(inv).leads_to(q)),
+        spec.entails(always(inv)),
+    ensures
+        spec.entails(p.leads_to(q)),
+{
+    assert forall |ex| #[trigger] spec.satisfied_by(ex) implies p.leads_to(q).satisfied_by(ex) by {
+        assert forall |i| #[trigger] p.satisfied_by(ex.suffix(i)) implies eventually(q).satisfied_by(ex.suffix(i)) by {
+            instantiate_entailed_always(ex, i, spec, inv);
+            instantiate_entailed_leads_to(ex, i, spec, p.and(inv), q);
+        }
+    }
+}
+
 }
diff --git a/src/v2/kubernetes_cluster/proof/controller_runtime_liveness.rs b/src/v2/kubernetes_cluster/proof/controller_runtime_liveness.rs
index 0395287c4..6ce1432ca 100644
--- a/src/v2/kubernetes_cluster/proof/controller_runtime_liveness.rs
+++ b/src/v2/kubernetes_cluster/proof/controller_runtime_liveness.rs
@@ -298,7 +298,7 @@ pub proof fn lemma_from_some_state_to_arbitrary_next_state(self, spec: TempPred<
             })
     };
     temp_pred_equality(lift_state(Self::pending_req_in_flight_or_resp_in_flight_at_reconcile_state(controller_id, cr.object_ref(), current_state)), lift_state(Self::at_expected_reconcile_states(controller_id, cr.object_ref(), current_state)).implies(lift_state(at_some_state_and_pending_req_in_flight_or_resp_in_flight)));
-    implies_to_leads_to(spec, lift_state(Self::at_expected_reconcile_states(controller_id, cr.object_ref(), current_state)), lift_state(at_some_state_and_pending_req_in_flight_or_resp_in_flight));
+    always_implies_to_leads_to(spec, lift_state(Self::at_expected_reconcile_states(controller_id, cr.object_ref(), current_state)), lift_state(at_some_state_and_pending_req_in_flight_or_resp_in_flight));
 
     let req_in_flight = Self::pending_req_in_flight_at_reconcile_state(controller_id, cr.object_ref(), current_state);
     let resp_in_flight = Self::resp_in_flight_matches_pending_req_at_reconcile_state(controller_id, cr.object_ref(), current_state);
@@ -306,7 +306,7 @@ pub proof fn lemma_from_some_state_to_arbitrary_next_state(self, spec: TempPred<
     self.lemma_from_in_flight_resp_matches_pending_req_at_some_state_to_next_state(spec, controller_id, cr, current_state, next_state);
     self.lemma_from_pending_req_in_flight_at_some_state_to_next_state(spec, controller_id, cr, current_state, next_state);
 
-    or_leads_to_combine_temp(spec, lift_state(req_in_flight), lift_state(resp_in_flight), lift_state(Self::at_expected_reconcile_states(controller_id, cr.object_ref(), next_state)));
+    or_leads_to_combine(spec, lift_state(req_in_flight), lift_state(resp_in_flight), lift_state(Self::at_expected_reconcile_states(controller_id, cr.object_ref(), next_state)));
     temp_pred_equality(lift_state(req_in_flight).or(lift_state(resp_in_flight)), lift_state(at_some_state_and_pending_req_in_flight_or_resp_in_flight));
     leads_to_trans_n!(
         spec,
@@ -336,7 +336,7 @@ pub proof fn lemma_from_init_state_to_next_state_to_reconcile_idle(self, spec: T
         &&& Self::no_pending_req_msg(controller_id, s, cr.object_ref())
     };
     temp_pred_equality(lift_state(Self::no_pending_req_msg_at_reconcile_state(controller_id, cr.object_ref(), init_state)), lift_state(Self::at_expected_reconcile_states(controller_id, cr.object_ref(), init_state)).implies(lift_state(no_pending_req)));
-    implies_to_leads_to(spec, lift_state(Self::at_expected_reconcile_states(controller_id, cr.object_ref(), init_state)), lift_state(no_pending_req));
+    always_implies_to_leads_to(spec, lift_state(Self::at_expected_reconcile_states(controller_id, cr.object_ref(), init_state)), lift_state(no_pending_req));
     let stronger_next = |s, s_prime| {
         &&& self.next()(s, s_prime)
         &&& Self::crash_disabled(controller_id)(s)
diff --git a/src/v2/kubernetes_cluster/proof/failures_liveness.rs b/src/v2/kubernetes_cluster/proof/failures_liveness.rs
index f8d76370f..2a2e846ad 100644
--- a/src/v2/kubernetes_cluster/proof/failures_liveness.rs
+++ b/src/v2/kubernetes_cluster/proof/failures_liveness.rs
@@ -33,7 +33,7 @@ pub proof fn lemma_true_leads_to_crash_always_disabled(self, spec: TempPred<Clus
         spec, lift_action(stronger_next), lift_action(self.next()),
         lift_state(Self::there_is_the_controller_state(controller_id))
     );
-    leads_to_stable_temp(spec, lift_action(stronger_next), true_pred(), lift_state(Self::crash_disabled(controller_id)));
+    leads_to_stable(spec, lift_action(stronger_next), true_pred(), lift_state(Self::crash_disabled(controller_id)));
 }
 
 pub open spec fn req_drop_disabled() -> StatePred<ClusterState> {
@@ -48,7 +48,7 @@ pub proof fn lemma_true_leads_to_req_drop_always_disabled(self, spec: TempPred<C
 {
     let true_state = |s: ClusterState| true;
     self.disable_req_drop().wf1((), spec, self.next(), true_state, Self::req_drop_disabled());
-    leads_to_stable_temp(spec, lift_action(self.next()), true_pred(), lift_state(Self::req_drop_disabled()));
+    leads_to_stable(spec, lift_action(self.next()), true_pred(), lift_state(Self::req_drop_disabled()));
 }
 
 }
diff --git a/src/v2/kubernetes_cluster/proof/garbage_collector.rs b/src/v2/kubernetes_cluster/proof/garbage_collector.rs
index 95adf9043..df241963d 100644
--- a/src/v2/kubernetes_cluster/proof/garbage_collector.rs
+++ b/src/v2/kubernetes_cluster/proof/garbage_collector.rs
@@ -212,7 +212,7 @@ pub proof fn lemma_eventually_objects_owner_references_satisfies(
             leads_to_trans_n!(spec, lift_state(pre), lift_state(delete_msg_in_flight), lift_state(post));
 
             temp_pred_equality(lift_state(Self::objects_owner_references_violates(key, eventual_owner_ref)).implies(lift_state(Self::garbage_collector_deletion_enabled(key))), lift_state(Self::objects_owner_references_violates(key, eventual_owner_ref)).implies(lift_state(pre)));
-            leads_to_weaken_temp(spec, lift_state(pre), lift_state(post), lift_state(Self::objects_owner_references_violates(key, eventual_owner_ref)), lift_state(post));
+            leads_to_weaken(spec, lift_state(pre), lift_state(post), lift_state(Self::objects_owner_references_violates(key, eventual_owner_ref)), lift_state(post));
         }
     );
 
@@ -231,7 +231,7 @@ pub proof fn lemma_eventually_objects_owner_references_satisfies(
         }
     }
 
-    leads_to_stable_temp(spec, lift_action(stronger_next), true_pred(), lift_state(post));
+    leads_to_stable(spec, lift_action(stronger_next), true_pred(), lift_state(post));
 }
 
 proof fn lemma_delete_msg_in_flight_leads_to_owner_references_satisfies(
diff --git a/src/v2/kubernetes_cluster/proof/network.rs b/src/v2/kubernetes_cluster/proof/network.rs
index da74d7ce2..b1b019633 100644
--- a/src/v2/kubernetes_cluster/proof/network.rs
+++ b/src/v2/kubernetes_cluster/proof/network.rs
@@ -404,7 +404,7 @@ pub proof fn lemma_always_every_in_flight_msg_has_unique_id(self, spec: TempPred
         assert forall |msg1, msg2| #[trigger] s.in_flight().contains(msg1) && #[trigger] s.in_flight().contains(msg2) && msg1 != msg2
         implies msg1.rpc_id != msg2.rpc_id by {}
     };
-    always_weaken_temp::<ClusterState>(spec, lift_state(Self::every_in_flight_msg_has_no_replicas_and_has_unique_id()), lift_state(Self::every_in_flight_msg_has_unique_id()));
+    always_weaken::<ClusterState>(spec, lift_state(Self::every_in_flight_msg_has_no_replicas_and_has_unique_id()), lift_state(Self::every_in_flight_msg_has_unique_id()));
 }
 
 }
diff --git a/src/v2/kubernetes_cluster/proof/network_liveness.rs b/src/v2/kubernetes_cluster/proof/network_liveness.rs
index 87aad43ec..1d1d4b5a2 100644
--- a/src/v2/kubernetes_cluster/proof/network_liveness.rs
+++ b/src/v2/kubernetes_cluster/proof/network_liveness.rs
@@ -177,17 +177,17 @@ pub proof fn lemma_some_rpc_id_leads_to_always_every_in_flight_req_msg_satisfies
 
             self.lemma_true_leads_to_always_no_req_before_rpc_id_is_in_flight(spec_with_rpc_id, rpc_id);
 
-            implies_preserved_by_always_temp(
+            entails_preserved_by_always(
                 lift_state(invariant),
                 lift_state(Self::no_req_before_rpc_id_is_in_flight(rpc_id))
                 .implies(lift_state(Self::every_in_flight_req_msg_satisfies(requirements)))
             );
-            valid_implies_trans(
+            entails_trans(
                 spec_with_rpc_id, always(lift_state(invariant)),
                 always(lift_state(Self::no_req_before_rpc_id_is_in_flight(rpc_id)).implies(lift_state(Self::every_in_flight_req_msg_satisfies(requirements))))
             );
-            always_implies_preserved_by_always_temp(spec_with_rpc_id, lift_state(Self::no_req_before_rpc_id_is_in_flight(rpc_id)), lift_state(Self::every_in_flight_req_msg_satisfies(requirements)));
-            leads_to_weaken_temp(
+            always_implies_preserved_by_always(spec_with_rpc_id, lift_state(Self::no_req_before_rpc_id_is_in_flight(rpc_id)), lift_state(Self::every_in_flight_req_msg_satisfies(requirements)));
+            leads_to_weaken(
                 spec_with_rpc_id,
                 true_pred(), always(lift_state(Self::no_req_before_rpc_id_is_in_flight(rpc_id))),
                 true_pred(), always(lift_state(Self::every_in_flight_req_msg_satisfies(requirements)))
@@ -201,7 +201,7 @@ pub proof fn lemma_some_rpc_id_leads_to_always_every_in_flight_req_msg_satisfies
         always(lift_state(Self::every_in_flight_req_msg_satisfies(requirements)))
     );
     temp_pred_equality(true_pred().and(lift_state(Self::rpc_id_counter_is(rpc_id))), lift_state(Self::rpc_id_counter_is(rpc_id)));
-    valid_implies_trans(spec, stable_spec, lift_state(Self::rpc_id_counter_is(rpc_id)).leads_to(always(lift_state(Self::every_in_flight_req_msg_satisfies(requirements)))));
+    entails_trans(spec, stable_spec, lift_state(Self::rpc_id_counter_is(rpc_id)).leads_to(always(lift_state(Self::every_in_flight_req_msg_satisfies(requirements)))));
 }
 
 // All the APIRequest messages with a smaller id than rpc_id will eventually leave the network.
@@ -231,7 +231,7 @@ pub proof fn lemma_true_leads_to_always_no_req_before_rpc_id_is_in_flight(self,
         }
     }
 
-    leads_to_stable_temp(spec, lift_action(stronger_next), true_pred(), lift_state(Self::no_req_before_rpc_id_is_in_flight(rpc_id)));
+    leads_to_stable(spec, lift_action(stronger_next), true_pred(), lift_state(Self::no_req_before_rpc_id_is_in_flight(rpc_id)));
 }
 
 pub proof fn lemma_eventually_no_req_before_rpc_id_is_in_flight(self, spec: TempPred<ClusterState>, rpc_id: RPCId)
@@ -294,7 +294,7 @@ proof fn lemma_pending_requests_number_is_n_leads_to_no_pending_requests(self, s
                 }
             }
         });
-        valid_implies_implies_leads_to(spec, lift_state(pending_requests_num_is_zero), lift_state(no_more_pending_requests));
+        entails_implies_leads_to(spec, lift_state(pending_requests_num_is_zero), lift_state(no_more_pending_requests));
     } else {
         // The induction step:
         // If we already have "there are msg_num-1 such requests" ~> "all such requests are gone" (the inductive hypothesis),
@@ -343,7 +343,7 @@ proof fn lemma_pending_requests_number_is_n_leads_to_no_pending_requests(self, s
         self.lemma_pending_requests_number_is_n_leads_to_no_pending_requests(
             spec, rpc_id, (msg_num - 1) as nat
         );
-        leads_to_trans_temp(
+        leads_to_trans(
             spec, pending_requests_num_is_msg_num, pending_requests_num_is_msg_num_minus_1, no_more_pending_requests
         );
     }
diff --git a/src/v2/kubernetes_cluster/proof/objects_in_store.rs b/src/v2/kubernetes_cluster/proof/objects_in_store.rs
index 5f32af86f..27c32fde6 100644
--- a/src/v2/kubernetes_cluster/proof/objects_in_store.rs
+++ b/src/v2/kubernetes_cluster/proof/objects_in_store.rs
@@ -238,7 +238,7 @@ pub proof fn lemma_always_each_object_in_etcd_is_well_formed<T: CustomResourceVi
     };
     entails_always_and_n!(spec, lift_state(p1), lift_state(p2));
     temp_pred_equality(lift_state(p1).and(lift_state(p2)), lift_state(p));
-    always_weaken_temp::<ClusterState>(spec, lift_state(p), lift_state(invariant));
+    always_weaken::<ClusterState>(spec, lift_state(p), lift_state(invariant));
 }
 
 }
diff --git a/src/v2/kubernetes_cluster/proof/wf1_helpers.rs b/src/v2/kubernetes_cluster/proof/wf1_helpers.rs
index 1c837ae6a..b5b472be4 100644
--- a/src/v2/kubernetes_cluster/proof/wf1_helpers.rs
+++ b/src/v2/kubernetes_cluster/proof/wf1_helpers.rs
@@ -38,7 +38,7 @@ pub proof fn lemma_pre_leads_to_post_by_api_server(
 {
     use_tla_forall::<ClusterState, Option<Message>>(spec, |i| self.api_server_next().weak_fairness(i), input);
     self.api_server_action_pre_implies_next_pre(step, input);
-    valid_implies_trans::<ClusterState>(
+    entails_trans::<ClusterState>(
         lift_state(pre),
         lift_state(self.api_server_action_pre(step, input)),
         lift_state(self.api_server_next().pre(input))
@@ -60,7 +60,7 @@ pub proof fn lemma_pre_leads_to_post_by_builtin_controllers(
 {
     use_tla_forall::<ClusterState, (BuiltinControllerChoice, ObjectRef)>(spec, |i| self.builtin_controllers_next().weak_fairness(i), input);
     self.builtin_controllers_action_pre_implies_next_pre(step, input);
-    valid_implies_trans::<ClusterState>(
+    entails_trans::<ClusterState>(
         lift_state(pre),
         lift_state(self.builtin_controllers_action_pre(step, input)),
         lift_state(self.builtin_controllers_next().pre(input))
@@ -82,7 +82,7 @@ pub proof fn lemma_pre_leads_to_post_by_controller(
 {
     use_tla_forall::<ClusterState, (Option<Message>, Option<ObjectRef>)>(spec, |i: (Option<Message>, Option<ObjectRef>)| self.controller_next().weak_fairness((controller_id, i.0, i.1)), input);
     self.controller_action_pre_implies_next_pre(step, (controller_id, input.0, input.1));
-    valid_implies_trans(
+    entails_trans(
         lift_state(pre),
         lift_state(self.controller_action_pre(step, (controller_id, input.0, input.1))),
         lift_state(self.controller_next().pre((controller_id, input.0, input.1)))
@@ -120,7 +120,7 @@ pub proof fn lemma_pre_leads_to_post_by_external(
 {
     use_tla_forall::<ClusterState, Option<Message>>(spec, |i| self.external_next().weak_fairness((controller_id, i)), input);
     self.external_action_pre_implies_next_pre(step, (controller_id, input));
-    valid_implies_trans::<ClusterState>(
+    entails_trans::<ClusterState>(
         lift_state(pre),
         lift_state(self.external_action_pre(step, (controller_id, input))),
         lift_state(self.external_next().pre((controller_id, input)))