From 52a3dc34dd27b2220ec267d24ad8e574fd18f952 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 3 Sep 2014 13:01:19 +0200
Subject: [PATCH] Prove Forall3_app.

---
 theories/list.v | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/theories/list.v b/theories/list.v
index 2df51d67..6e1ce23c 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -2341,6 +2341,10 @@ End Forall2_order.
 
 Section Forall3.
   Context {A B C} (P : A → B → C → Prop).
+  Lemma Forall3_app l1 k1 k1' l2 k2 k2' :
+    Forall3 P l1 k1 k1' → Forall3 P l2 k2 k2' →
+    Forall3 P (l1 ++ l2) (k1 ++ k2) (k1' ++ k2').
+  Proof. induction 1; simpl; [done|constructor]; auto. Qed.
   Lemma Forall3_impl (Q : A → B → C → Prop) l l' k :
     Forall3 P l l' k → (∀ x y z, P x y z → Q x y z) → Forall3 Q l l' k.
   Proof. intros Hl ?. induction Hl; constructor; auto. Defined.
-- 
GitLab