Implement alternative lemma rule?

[skeuchel]

Currently, the Hoare triple define this rule for the lemma ghost statement

    | rule_stm_lemmak
        {Δ} {l : 𝑳 Δ} (es : NamedEnv (Exp Γ) Δ) (k : Stm Γ τ)
        (P Q : L) (R : Lit τ -> CStore Γ -> L) :
        LTriple (evals es δ) P Q (LEnv l) ->
        δ ⊢ ⦃ Q ⦄ k ⦃ R ⦄ ->
        δ ⊢ ⦃ P ⦄ stm_lemmak l es k ⦃ R ⦄

However, it should be perfectly fine to ignore the lemma and instead use

    | rule_stm_lemmak2
        {Δ} {l : 𝑳 Δ} (es : NamedEnv (Exp Γ) Δ) (k : Stm Γ τ)
        (P : L) (R : Lit τ -> CStore Γ -> L) :
        δ ⊢ ⦃ P ⦄ k ⦃ R ⦄ ->
        δ ⊢ ⦃ P ⦄ stm_lemmak l es k ⦃ R ⦄

The former rule_stm_lemmak is derivable from the latter rule_stm_lemmak2 via consequence and potentially some rewiring.