case mk.mk
α : Type u
β : α → Type v
C : Finmap β → Prop
H : ∀ (a : AList β), C ⟦a⟧
entries✝ : Multiset (Sigma β)
a : List (Sigma β)
h : Multiset.NodupKeys (Quot.mk Setoid.r a)
⊢ C { entries := Quot.mk Setoid.r a, nodupKeys := h }
α : Type u
β : α → Type v
C : Finmap β → Prop
s : Finmap β
H : ∀ (a : AList β), C ⟦a⟧
⊢ C s
rcases s with ⟨⟨a⟩, h⟩
no goals
case mk.mk
α : Type u
β : α → Type v
C : Finmap β → Prop
H : ∀ (a : AList β), C ⟦a⟧
entries✝ : Multiset (Sigma β)
a : List (Sigma β)
h : Multiset.NodupKeys (Quot.mk Setoid.r a)
⊢ C { entries := Quot.mk Setoid.r a, nodupKeys := h }
exact H ⟨a, h⟩