K : Option Γ' → Finset Λ'
S : Finset Λ'
⊢ (∀ (q : Λ') (x : Option Γ'), q ∈ K x → TM2.SupportsStmt S (tr q)) ↔
    ∀ (a : Option Γ') (q : Λ'), q ∈ K a → TM2.SupportsStmt S (tr q)
K : Option Γ' → Finset Λ'
S : Finset Λ'
⊢ Supports (Finset.biUnion Finset.univ K) S ↔ ∀ (a : Option Γ'), Supports (K a) S
simp [Supports]
no goals
K : Option Γ' → Finset Λ'
S : Finset Λ'
⊢ (∀ (q : Λ') (x : Option Γ'), q ∈ K x → TM2.SupportsStmt S (tr q)) ↔
    ∀ (a : Option Γ') (q : Λ'), q ∈ K a → TM2.SupportsStmt S (tr q)
apply forall_swap