simp[e]
α✝ : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁹ : Primcodable α✝
inst✝⁸ : Primcodable α₁
inst✝⁷ : Primcodable α₂
inst✝⁶ : Primcodable β
inst✝⁵ : Primcodable γ
inst✝⁴ : Primcodable σ
inst✝³ : Primcodable τ
α : Type u_8
inst✝² : Primcodable α
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
hsup : Primrec₂ Sup.sup
e : ∀ (l : List α), l.sup = List.foldr Sup.sup ⊥ l
this : Primrec fun l => List.foldr Sup.sup ⊥ l
⊢ ∀ (n : List α), List.foldr Sup.sup ⊥ n = n.sup
no goals