no goals
α : Type u_1
β : Type ?u.105197
β₂ : Type ?u.105200
γ : Type ?u.105203
ι : Sort ?u.105206
ι' : Sort ?u.105209
κ : ι → Sort ?u.105214
κ' : ι' → Sort ?u.105219
inst✝ : CompleteLattice α
f g s✝ t : ι → α
a b : α
s : False → α
⊢ iInf s = ⊤
simp