Generalize Forall2_forall_iff

1 files changed, 8 insertions, 4 deletions

diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v
index ee4fb0b9b..38678ac59 100644
--- a/src/Util/ListUtil.v
+++ b/src/Util/ListUtil.v
@@ -1654,10 +1654,10 @@ Proof.
   rewrite fold_right_andb_true_map_iff, fold_right_and_True_forall_In_iff; reflexivity.
 Qed.
 
-Lemma Forall2_forall_iff : forall {A} R (xs ys : list A) d, length xs = length ys ->
-  (Forall2 R xs ys <-> (forall i, (i < length xs)%nat -> R (nth_default d xs i) (nth_default d ys i))).
+Lemma Forall2_forall_iff : forall {A B} (R : A -> B -> Prop) (xs : list A) (ys : list B) d1 d2, length xs = length ys ->
+  (Forall2 R xs ys <-> (forall i, (i < length xs)%nat -> R (nth_default d1 xs i) (nth_default d2 ys i))).
 Proof.
-  intros A R xs ys d H; split; [ intros H0 i H1 | intros H0 ].
+  intros A B R xs ys d1 d2 H; split; [ intros H0 i H1 | intros H0 ].
 
   + revert xs ys H H0 H1.
     induction i as [|i IHi]; intros xs ys H H0 H1; destruct H0; distr_length; autorewrite with push_nth_default; auto.
@@ -1673,6 +1673,10 @@ Proof.
       apply H0; omega.
 Qed.
 
+Lemma Forall2_forall_iff' : forall {A} R (xs ys : list A) d, length xs = length ys ->
+  (Forall2 R xs ys <-> (forall i, (i < length xs)%nat -> R (nth_default d xs i) (nth_default d ys i))).
+Proof. intros; apply Forall2_forall_iff; assumption. Qed.
+
 Lemma nth_default_firstn : forall {A} (d : A) l i n,
   nth_default d (firstn n l) i = if le_dec n (length l)
                                  then if lt_dec i n then nth_default d l i else d
@@ -1774,4 +1778,4 @@ Lemma map2_map {A B C A' B'} (f:A -> B -> C) (g:A' -> A) (h:B' -> B) (xs:list A'
 Proof.
   revert ys; induction xs as [|a xs IHxs]; destruct ys; intros; try reflexivity; [].
   simpl. rewrite IHxs. reflexivity.
-Qed.
\ No newline at end of file
+Qed.