proposition: Lemma fold_nexts_equiv ps1 ps2 ss1 ss2 : pequiv ps1 ps2 -> lequiv ss1 ss2 -> pequiv (fold_left nexts (snd ps1) (fst ps1, ss1)) (fold_left nexts (snd ps2) (fst ps2, ss2)).
proof: Proof. unfold pequiv, lequiv; intros (He1, He2) He3. case (fold_nexts_correct ps1 ss1); intros Hr1 Hs1. case (fold_nexts_correct ps2 ss2); intros Hr2 Hs2. split; intros s. - apply iff_trans with (1 := Hr1 s). apply iff_sym; apply iff_trans with (1 := Hr2 s). split; intros [H1 | H1]; auto. + left; rewrite He1; auto. + right; case H1; intros f (i, (Hf1, (Hf2, (Hf3, Hf4)))). exists f; exists i; repeat split; try rewrite He2; try rewrite He1; auto. + left; rewrite <- He1; auto. + right; case H1; intros f (i, (Hf1, (Hf2, (Hf3, Hf4)))). exists f; exists i; repeat split; try rewrite <- He2; try rewrite <- He1; auto. - apply iff_trans with (1 := Hs1 s). apply iff_sym; apply iff_trans with (1 := Hs2 s). split; intros [H1 | H1]; auto. + left; rewrite He3; auto. + right; case H1; intros f (i, (Hf1, (Hf2, (Hf3, Hf4)))). exists f; exists i; repeat split; try rewrite He2; try rewrite He1; auto. + left; rewrite <- He3; auto. + right; case H1; intros f (i, (Hf1, (Hf2, (Hf3, Hf4)))). exists f; exists i; repeat split; try rewrite <- He2; try rewrite <- He1; auto. Qed.
imports: ZArith List