simp[e]
α✝ : 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₂
no goals