case zero
α : Type u_1
β : Type u_2
γ : Type ?u.439795
δ : Type ?u.439798
r : α → β → Prop
p : γ → δ → Prop
s : Multiset α
t : Multiset β
u : Multiset α
v : Multiset β
huv : Rel r u v
⊢ Rel r (0 + u) (0 + v)

case cons
α : Type u_1
β : Type u_2
γ : Type ?u.439795
δ : Type ?u.439798
r : α → β → Prop
p : γ → δ → Prop
s : Multiset α
t : Multiset β
u : Multiset α
v : Multiset β
huv : Rel r u v
a✝² : α
b✝ : β
as✝ : Multiset α
bs✝ : Multiset β
a✝¹ : r a✝² b✝
a✝ : Rel r as✝ bs✝
a_ih✝ : Rel r (as✝ + u) (bs✝ + v)
⊢ Rel r (a✝² ::ₘ as✝ + u) (b✝ ::ₘ bs✝ + v)
α : Type u_1
β : Type u_2
γ : Type ?u.439795
δ : Type ?u.439798
r : α → β → Prop
p : γ → δ → Prop
s : Multiset α
t : Multiset β
u : Multiset α
v : Multiset β
hst : Rel r s t
huv : Rel r u v
⊢ Rel r (s + u) (t + v)
induction hst
case cons
α : Type u_1
β : Type u_2
γ : Type ?u.439795
δ : Type ?u.439798
r : α → β → Prop
p : γ → δ → Prop
s : Multiset α
t : Multiset β
u : Multiset α
v : Multiset β
huv : Rel r u v
a✝² : α
b✝ : β
as✝ : Multiset α
bs✝ : Multiset β
a✝¹ : r a✝² b✝
a✝ : Rel r as✝ bs✝
a_ih✝ : Rel r (as✝ + u) (bs✝ + v)
⊢ Rel r (a✝² ::ₘ as✝ + u) (b✝ ::ₘ bs✝ + v)
case zero
α : Type u_1
β : Type u_2
γ : Type ?u.439795
δ : Type ?u.439798
r : α → β → Prop
p : γ → δ → Prop
s : Multiset α
t : Multiset β
u : Multiset α
v : Multiset β
huv : Rel r u v
⊢ Rel r (0 + u) (0 + v)

case cons
α : Type u_1
β : Type u_2
γ : Type ?u.439795
δ : Type ?u.439798
r : α → β → Prop
p : γ → δ → Prop
s : Multiset α
t : Multiset β
u : Multiset α
v : Multiset β
huv : Rel r u v
a✝² : α
b✝ : β
as✝ : Multiset α
bs✝ : Multiset β
a✝¹ : r a✝² b✝
a✝ : Rel r as✝ bs✝
a_ih✝ : Rel r (as✝ + u) (bs✝ + v)
⊢ Rel r (a✝² ::ₘ as✝ + u) (b✝ ::ₘ bs✝ + v)
case zero => simpa using huv
no goals
case cons
α : Type u_1
β : Type u_2
γ : Type ?u.439795
δ : Type ?u.439798
r : α → β → Prop
p : γ → δ → Prop
s : Multiset α
t : Multiset β
u : Multiset α
v : Multiset β
huv : Rel r u v
a✝² : α
b✝ : β
as✝ : Multiset α
bs✝ : Multiset β
a✝¹ : r a✝² b✝
a✝ : Rel r as✝ bs✝
a_ih✝ : Rel r (as✝ + u) (bs✝ + v)
⊢ Rel r (a✝² ::ₘ as✝ + u) (b✝ ::ₘ bs✝ + v)
case cons a b s t hab hst ih => simpa using ih.cons hab
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.439795
δ : Type ?u.439798
r : α → β → Prop
p : γ → δ → Prop
s : Multiset α
t : Multiset β
u : Multiset α
v : Multiset β
huv : Rel r u v
⊢ Rel r (0 + u) (0 + v)
simpa using huv
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.439795
δ : Type ?u.439798
r : α → β → Prop
p : γ → δ → Prop
s✝ : Multiset α
t✝ : Multiset β
u : Multiset α
v : Multiset β
huv : Rel r u v
a : α
b : β
s : Multiset α
t : Multiset β
hab : r a b
hst : Rel r s t
ih : Rel r (s + u) (t + v)
⊢ Rel r (a ::ₘ s + u) (b ::ₘ t + v)
simpa using ih.cons hab