Theorems specialized for state predicates. Their premises are typically pure Lean propositions involving states before/after an action, instead of being in the form of |-tla-.

theorem TLA.state_preds_and {σ : Type u} (p q : σ → Prop) : (⌜ p ⌝ ∧ ⌜ q ⌝) =tla= (⌜ fun (s : σ) => p s ∧ q s ⌝)

theorem TLA.init_invariant {σ : Type u} {init : σ → Prop} {next : action σ} {inv : σ → Prop} (hinit : ∀ (s : σ), init s → inv s) (hnext : ∀ (s s' : σ), next s s' → inv s → inv s') : (⌜ init ⌝ ∧ □⟨ next ⟩) |-tla- (□⌜ inv ⌝)