α : Type ?u.126304
β : Type ?u.126307
γ : Type ?u.126310
⊢ univ.val = True ::ₘ {False}
α : Type ?u.126304
β : Type ?u.126307
γ : Type ?u.126310
⊢ univ.val = {True, False}.val
simp
no goals
α : Type ?u.126304
β : Type ?u.126307
γ : Type ?u.126310
⊢ univ.val = True ::ₘ {False}
rfl