Theorem: List.subset_of_eq (Logic/Vorspiel/Vorspiel.lean)

State before:
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.171524 → Type ?u.171526
α : Type u_1
β : Type ?u.171532
inst✝ : Monad m
l₁ l₂ : List α
e : l₁ = l₂
⊢ l₁ ⊆ l₂
Tactic:
simp[e]
State after:
no goals