Theorems about the leads-to operator.

theorem TLA.leads_to_exists {σ : Type u} {α : Sort u_1} (Γ q : pred σ) (p : α → pred σ) : (∀ (x : α), (Γ) |-tla- ((p x) ↝ q)) ↔ (Γ) |-tla- (∃ x, (p x) ↝ q)

theorem TLA.leads_to_pure_pred_and {σ : Type u} (Γ p q : pred σ) (φ : Prop) : φ → (Γ) |-tla- (p ↝ q) ↔ (Γ) |-tla- (⌞ φ ⌟ ∧ p ↝ q)

theorem TLA.leads_to_conseq {σ : Type u} (p p' q q' : pred σ) : |-tla- (p' ⇒ p → q ⇒ q' → p ↝ q ⇒ p' ↝ q')

theorem TLA.leads_to_trans {σ : Type u} (p q r : pred σ) : |-tla- (p ↝ q → q ↝ r → p ↝ r)

theorem TLA.leads_to_combine {σ : Type u} (Γ Γ' p1 q1 p2 q2 : pred σ) (h1 : (□Γ ∧ Γ') |-tla- (p1 ↝ q1)) (h2 : (□Γ ∧ Γ') |-tla- (p2 ↝ q2)) (h1' : (q1 ∧ □Γ) |-tla- (□q1)) (h2' : (q2 ∧ □Γ) |-tla- (□q2)) : (□Γ ∧ Γ') |-tla- (p1 ∧ p2 ↝ q1 ∧ q2)

theorem TLA.leads_to_strengthen_lhs {σ : Type u} (p q inv : pred σ) : |-tla- (□inv → p ∧ inv ↝ q → p ↝ q)