Theorem: DVect2.append_nil (Moncalc/Data/DVect2/Basic.lean)

State before:
α : Type u₁
β : Type u₂
γ : α → β → Type v
head✝¹ : α
tail✝¹ : List α
head✝ : β
tail✝ : List β
f : γ head✝¹ head✝
fs : DVect2 γ tail✝¹ tail✝
⊢ cons f fs ++ nil ≡ cons f fs
Tactic:
rw [cons_append]
State after:
α : Type u₁
β : Type u₂
γ : α → β → Type v
head✝¹ : α
tail✝¹ : List α
head✝ : β
tail✝ : List β
f : γ head✝¹ head✝
fs : DVect2 γ tail✝¹ tail✝
⊢ cons f (fs ++ nil) ≡ cons f fs

State before:
α : Type u₁
β : Type u₂
γ : α → β → Type v
head✝¹ : α
tail✝¹ : List α
head✝ : β
tail✝ : List β
f : γ head✝¹ head✝
fs : DVect2 γ tail✝¹ tail✝
⊢ cons f (fs ++ nil) ≡ cons f fs
Tactic:
exact DVect2.Eq.descend rfl (append_nil fs)
State after:
no goals