case zero
α : Type u_1
β : Type u_2
γ : Type ?u.439427
δ : Type ?u.439430
r✝ : α → β → Prop
p✝ : γ → δ → Prop
r p : α → β → Prop
s : Multiset α
t : Multiset β
h : ∀ (a : α), a ∈ 0 → ∀ (b : β), b ∈ 0 → r a b → p a b
⊢ Rel p 0 0

case cons
α : Type u_1
β : Type u_2
γ : Type ?u.439427
δ : Type ?u.439430
r✝ : α → β → Prop
p✝ : γ → δ → Prop
r p : α → β → Prop
s : Multiset α
t : Multiset β
a✝² : α
b✝ : β
as✝ : Multiset α
bs✝ : Multiset β
a✝¹ : r a✝² b✝
a✝ : Rel r as✝ bs✝
a_ih✝ : (∀ (a : α), a ∈ as✝ → ∀ (b : β), b ∈ bs✝ → r a b → p a b) → Rel p as✝ bs✝
h : ∀ (a : α), a ∈ a✝² ::ₘ as✝ → ∀ (b : β), b ∈ b✝ ::ₘ bs✝ → r a b → p a b
⊢ Rel p (a✝² ::ₘ as✝) (b✝ ::ₘ bs✝)
α : Type u_1
β : Type u_2
γ : Type ?u.439427
δ : Type ?u.439430
r✝ : α → β → Prop
p✝ : γ → δ → Prop
r p : α → β → Prop
s : Multiset α
t : Multiset β
hst : Rel r s t
h : ∀ (a : α), a ∈ s → ∀ (b : β), b ∈ t → r a b → p a b
⊢ Rel p s t
induction hst
case cons
α : Type u_1
β : Type u_2
γ : Type ?u.439427
δ : Type ?u.439430
r✝ : α → β → Prop
p✝ : γ → δ → Prop
r p : α → β → Prop
s : Multiset α
t : Multiset β
a✝² : α
b✝ : β
as✝ : Multiset α
bs✝ : Multiset β
a✝¹ : r a✝² b✝
a✝ : Rel r as✝ bs✝
a_ih✝ : (∀ (a : α), a ∈ as✝ → ∀ (b : β), b ∈ bs✝ → r a b → p a b) → Rel p as✝ bs✝
h : ∀ (a : α), a ∈ a✝² ::ₘ as✝ → ∀ (b : β), b ∈ b✝ ::ₘ bs✝ → r a b → p a b
⊢ Rel p (a✝² ::ₘ as✝) (b✝ ::ₘ bs✝)
case zero
α : Type u_1
β : Type u_2
γ : Type ?u.439427
δ : Type ?u.439430
r✝ : α → β → Prop
p✝ : γ → δ → Prop
r p : α → β → Prop
s : Multiset α
t : Multiset β
h : ∀ (a : α), a ∈ 0 → ∀ (b : β), b ∈ 0 → r a b → p a b
⊢ Rel p 0 0

case cons
α : Type u_1
β : Type u_2
γ : Type ?u.439427
δ : Type ?u.439430
r✝ : α → β → Prop
p✝ : γ → δ → Prop
r p : α → β → Prop
s : Multiset α
t : Multiset β
a✝² : α
b✝ : β
as✝ : Multiset α
bs✝ : Multiset β
a✝¹ : r a✝² b✝
a✝ : Rel r as✝ bs✝
a_ih✝ : (∀ (a : α), a ∈ as✝ → ∀ (b : β), b ∈ bs✝ → r a b → p a b) → Rel p as✝ bs✝
h : ∀ (a : α), a ∈ a✝² ::ₘ as✝ → ∀ (b : β), b ∈ b✝ ::ₘ bs✝ → r a b → p a b
⊢ Rel p (a✝² ::ₘ as✝) (b✝ ::ₘ bs✝)
case zero => exact Rel.zero
no goals
case cons
α : Type u_1
β : Type u_2
γ : Type ?u.439427
δ : Type ?u.439430
r✝ : α → β → Prop
p✝ : γ → δ → Prop
r p : α → β → Prop
s : Multiset α
t : Multiset β
a✝² : α
b✝ : β
as✝ : Multiset α
bs✝ : Multiset β
a✝¹ : r a✝² b✝
a✝ : Rel r as✝ bs✝
a_ih✝ : (∀ (a : α), a ∈ as✝ → ∀ (b : β), b ∈ bs✝ → r a b → p a b) → Rel p as✝ bs✝
h : ∀ (a : α), a ∈ a✝² ::ₘ as✝ → ∀ (b : β), b ∈ b✝ ::ₘ bs✝ → r a b → p a b
⊢ Rel p (a✝² ::ₘ as✝) (b✝ ::ₘ bs✝)
case
  cons a b s t hab _hst ih =>
  apply Rel.cons (h a (mem_cons_self _ _) b (mem_cons_self _ _) hab)
  exact ih fun a' ha' b' hb' h' => h a' (mem_cons_of_mem ha') b' (mem_cons_of_mem hb') h'
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.439427
δ : Type ?u.439430
r✝ : α → β → Prop
p✝ : γ → δ → Prop
r p : α → β → Prop
s : Multiset α
t : Multiset β
h : ∀ (a : α), a ∈ 0 → ∀ (b : β), b ∈ 0 → r a b → p a b
⊢ Rel p 0 0
exact Rel.zero
α : Type u_1
β : Type u_2
γ : Type ?u.439427
δ : Type ?u.439430
r✝ : α → β → Prop
p✝ : γ → δ → Prop
r p : α → β → Prop
s✝ : Multiset α
t✝ : Multiset β
a : α
b : β
s : Multiset α
t : Multiset β
hab : r a b
_hst : Rel r s t
ih : (∀ (a : α), a ∈ s → ∀ (b : β), b ∈ t → r a b → p a b) → Rel p s t
h : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → ∀ (b_1 : β), b_1 ∈ b ::ₘ t → r a_1 b_1 → p a_1 b_1
⊢ Rel p s t
α : Type u_1
β : Type u_2
γ : Type ?u.439427
δ : Type ?u.439430
r✝ : α → β → Prop
p✝ : γ → δ → Prop
r p : α → β → Prop
s✝ : Multiset α
t✝ : Multiset β
a : α
b : β
s : Multiset α
t : Multiset β
hab : r a b
_hst : Rel r s t
ih : (∀ (a : α), a ∈ s → ∀ (b : β), b ∈ t → r a b → p a b) → Rel p s t
h : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → ∀ (b_1 : β), b_1 ∈ b ::ₘ t → r a_1 b_1 → p a_1 b_1
⊢ Rel p (a ::ₘ s) (b ::ₘ t)
apply Rel.cons (h a (mem_cons_self _ _) b (mem_cons_self _ _) hab)
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.439427
δ : Type ?u.439430
r✝ : α → β → Prop
p✝ : γ → δ → Prop
r p : α → β → Prop
s✝ : Multiset α
t✝ : Multiset β
a : α
b : β
s : Multiset α
t : Multiset β
hab : r a b
_hst : Rel r s t
ih : (∀ (a : α), a ∈ s → ∀ (b : β), b ∈ t → r a b → p a b) → Rel p s t
h : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → ∀ (b_1 : β), b_1 ∈ b ::ₘ t → r a_1 b_1 → p a_1 b_1
⊢ Rel p s t
exact ih fun a' ha' b' hb' h' => h a' (mem_cons_of_mem ha') b' (mem_cons_of_mem hb') h'