α : Type u_1
β : Type u_2
γ : Type ?u.131498
δ : Type ?u.131501
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l : List α
l₁ l₂ : List β
h : Forall₂ R l (l₁ ++ l₂)
h' : Forall₂ R (take (length l₁) l) (take (length l₁) (l₁ ++ l₂))
⊢ Forall₂ R (take (length l₁) l) l₁
α : Type u_1
β : Type u_2
γ : Type ?u.131498
δ : Type ?u.131501
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l : List α
l₁ l₂ : List β
h : Forall₂ R l (l₁ ++ l₂)
⊢ Forall₂ R (take (length l₁) l) l₁
have h' : Forall₂ R (take (length l₁) l) (take (length l₁) (l₁ ++ l₂)) :=
  forall₂_take (length l₁) h
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.131498
δ : Type ?u.131501
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l : List α
l₁ l₂ : List β
h : Forall₂ R l (l₁ ++ l₂)
h' : Forall₂ R (take (length l₁) l) (take (length l₁) (l₁ ++ l₂))
⊢ Forall₂ R (take (length l₁) l) l₁
rwa [take_left] at h'