added tcforall2_forall lemma

81f9b193 · Michael Sammler · 7e0096d8 · 81f9b193
Commit 81f9b193 authored Jan 30, 2020 by Michael Sammler
Hide whitespace changes
Inline Side-by-side

Showing with 3 additions and 0 deletions

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

No files found.
--- a/theories/list.v
+++ b/theories/list.v
@@ -3963,6 +3963,9 @@ Instance TCForall_app {A} (P : A → Prop) xs ys :
  TCForall P xs → TCForall P ys → TCForall P (xs ++ ys).
 Proof. rewrite !TCForall_Forall. apply Forall_app_2. Qed.

+Lemma TCForall2_Forall2 {A B} (P : A → B → Prop) xs ys : TCForall2 P xs ys ↔ Forall2 P xs ys.
+Proof. split; induction 1; constructor; auto. Qed.
+
 Section positives_flatten_unflatten.
  Local Open Scope positive_scope.