case mp
α : Type u_1
β : Type ?u.439191
γ : Type ?u.439194
δ : Type ?u.439197
r : α → β → Prop
p : γ → δ → Prop
s t : Multiset α
⊢ Rel (fun x x_1 => x = x_1) s t → s = t

case mpr
α : Type u_1
β : Type ?u.439191
γ : Type ?u.439194
δ : Type ?u.439197
r : α → β → Prop
p : γ → δ → Prop
s t : Multiset α
⊢ s = t → Rel (fun x x_1 => x = x_1) s t
α : Type u_1
β : Type ?u.439191
γ : Type ?u.439194
δ : Type ?u.439197
r : α → β → Prop
p : γ → δ → Prop
s t : Multiset α
⊢ Rel (fun x x_1 => x = x_1) s t ↔ s = t
constructor
case mp
α : Type u_1
β : Type ?u.439191
γ : Type ?u.439194
δ : Type ?u.439197
r : α → β → Prop
p : γ → δ → Prop
s t : Multiset α
h : Rel (fun x x_1 => x = x_1) s t
⊢ s = t
case mp
α : Type u_1
β : Type ?u.439191
γ : Type ?u.439194
δ : Type ?u.439197
r : α → β → Prop
p : γ → δ → Prop
s t : Multiset α
⊢ Rel (fun x x_1 => x = x_1) s t → s = t
intro h
no goals
case mp
α : Type u_1
β : Type ?u.439191
γ : Type ?u.439194
δ : Type ?u.439197
r : α → β → Prop
p : γ → δ → Prop
s t : Multiset α
h : Rel (fun x x_1 => x = x_1) s t
⊢ s = t
induction h <;> simp [*]
case mpr
α : Type u_1
β : Type ?u.439191
γ : Type ?u.439194
δ : Type ?u.439197
r : α → β → Prop
p : γ → δ → Prop
s t : Multiset α
h : s = t
⊢ Rel (fun x x_1 => x = x_1) s t
case mpr
α : Type u_1
β : Type ?u.439191
γ : Type ?u.439194
δ : Type ?u.439197
r : α → β → Prop
p : γ → δ → Prop
s t : Multiset α
⊢ s = t → Rel (fun x x_1 => x = x_1) s t
intro h
case mpr
α : Type u_1
β : Type ?u.439191
γ : Type ?u.439194
δ : Type ?u.439197
r : α → β → Prop
p : γ → δ → Prop
s : Multiset α
⊢ Rel (fun x x_1 => x = x_1) s s
case mpr
α : Type u_1
β : Type ?u.439191
γ : Type ?u.439194
δ : Type ?u.439197
r : α → β → Prop
p : γ → δ → Prop
s t : Multiset α
h : s = t
⊢ Rel (fun x x_1 => x = x_1) s t
subst h
no goals
case mpr
α : Type u_1
β : Type ?u.439191
γ : Type ?u.439194
δ : Type ?u.439197
r : α → β → Prop
p : γ → δ → Prop
s : Multiset α
⊢ Rel (fun x x_1 => x = x_1) s s
exact rel_eq_refl