Prove Forall3_app.

52a3dc34 · Robbert Krebbers · dbbda8cb · 52a3dc34
Commit 52a3dc34 authored Sep 03, 2014 by Robbert Krebbers
Hide whitespace changes
Inline Side-by-side

Showing with 4 additions and 0 deletions

theories/list.v theories/list.v +4 -0

No files found.
--- 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.