Commit 070f2235 authored by Robbert Krebbers's avatar Robbert Krebbers

Merge branch 'tcforall2_forall' into 'master'

Added TCForall2_Forall2 lemma

See merge request !107
parents 7e0096d8 81f9b193
Pipeline #23360 passed with stage
in 9 minutes and 38 seconds
......@@ -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.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment