Theorem: HTPI.seq_def (HTPILib/Chap8Part2.lean)

State before:
U : Type
A : Set U
l : List U
⊢ l ∈ seq A ↔ ∀ x ∈ l, x ∈ A
Tactic:
rfl
State after:
no goals