no goals
α : Type u_1
β : Type u_2
γ : Type ?u.129991
δ : Type ?u.129994
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
x✝¹ : List α
x✝ : List β
h : Forall₂ R x✝¹ x✝
⊢ Forall₂ R (drop 0 x✝¹) (drop 0 x✝)
simp only [drop, h]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.129991
δ : Type ?u.129994
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
n✝ : ℕ
⊢ Forall₂ R (drop (n✝ + 1) []) (drop (n✝ + 1) [])
simp only [Forall₂.nil, drop]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.129991
δ : Type ?u.129994
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
n : ℕ
a✝ : α
b✝ : β
l₁✝ : List α
l₂✝ : List β
h₁ : R a✝ b✝
h₂ : Forall₂ R l₁✝ l₂✝
⊢ Forall₂ R (drop (n + 1) (a✝ :: l₁✝)) (drop (n + 1) (b✝ :: l₂✝))
simp [And.intro h₁ h₂, forall₂_drop n]