diff --git a/theories/program_logic/total_lifting.v b/theories/program_logic/total_lifting.v index dc6f8e3ecd6ecaabbc4d359b7001401b4f6197ea..4b1335d9387cbd6554412fc315df999241ebfa61 100644 --- a/theories/program_logic/total_lifting.v +++ b/theories/program_logic/total_lifting.v @@ -24,7 +24,7 @@ Proof. by rewrite twp_unfold /twp_pre=> ->. Qed. Lemma twp_lift_pure_step `{Inhabited (state Λ)} s E Φ e1 : (∀ σ1, reducible_no_obs e1 σ1) → - (∀ σ1 κ e2 σ2 efs, prim_step e1 σ1 κ e2 σ2 efs → κ = [] /\ σ1 = σ2) → + (∀ σ1 κ e2 σ2 efs, prim_step e1 σ1 κ e2 σ2 efs → κ = [] ∧ σ1 = σ2) → (|={E}=> ∀ κ e2 efs σ, ⌜prim_step e1 σ κ e2 σ efs⌝ → WP e2 @ s; E [{ Φ }] ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ [{ _, True }]) ⊢ WP e1 @ s; E [{ Φ }]. @@ -61,7 +61,7 @@ Qed. Lemma twp_lift_pure_det_step `{Inhabited (state Λ)} {s E Φ} e1 e2 efs : (∀ σ1, reducible_no_obs e1 σ1) → - (∀ σ1 κ e2' σ2 efs', prim_step e1 σ1 κ e2' σ2 efs' → κ = [] /\ σ1 = σ2 ∧ e2 = e2' ∧ efs = efs')→ + (∀ σ1 κ e2' σ2 efs', prim_step e1 σ1 κ e2' σ2 efs' → κ = [] ∧ σ1 = σ2 ∧ e2 = e2' ∧ efs = efs')→ (|={E}=> WP e2 @ s; E [{ Φ }] ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ [{ _, True }]) ⊢ WP e1 @ s; E [{ Φ }]. Proof.