α : Type u_1
β : Type u_2
n : Nat
inst✝¹ : BEq α
inst✝ : Hashable α
⊢ WF
    (let nbuckets := numBucketsForCapacity n;
    let n_1 :=
      if h : nbuckets = 0 then { val := 8, property := empty.proof_1 }
      else { val := nbuckets, property := (_ : 0 < nbuckets) };
    Imp.empty' n_1.val)
α : Type u_1
β : Type u_2
n : Nat
inst✝¹ : BEq α
inst✝ : Hashable α
⊢ WF (Imp.empty n)
unfold empty
no goals
α : Type u_1
β : Type u_2
n : Nat
inst✝¹ : BEq α
inst✝ : Hashable α
⊢ WF
    (let nbuckets := numBucketsForCapacity n;
    let n_1 :=
      if h : nbuckets = 0 then { val := 8, property := empty.proof_1 }
      else { val := nbuckets, property := (_ : 0 < nbuckets) };
    Imp.empty' n_1.val)
apply empty'