proposition: Lemma fold_next2s_equiv p ps1 ps2 ss1 ss2 : tequiv ps1 ps2 -> lequiv ss1 ss2 -> tequiv (fold_left (next2s p) (snd ps1) (fst ps1, ss1)) (fold_left (next2s p) (snd ps2) (fst ps2, ss2)).
proof: Proof. unfold tequiv, lequiv. intros (He1, (He2, He3)) He4. case (fold_next2s_correct p ps1 ss1); intros Hr1 (Hs1, Ht1). case (fold_next2s_correct p ps2 ss2); intros Hr2 (Hs2, Ht2). split; [idtac | split]; intros s. apply iff_trans with (1 := Hr1 s); clear Hr1 Hs1 Ht1. apply iff_sym; apply iff_trans with (1 := Hr2 s); clear Hr2 Hs2 Ht2. split; intros [H1 | H1]; auto. left; rewrite He1; auto. right; case H1; intros f (i, (Hf1, (Hf2, (Hf3, (Hf4, Hf5))))). exists f; exists i; repeat split; try rewrite He2; try rewrite He1; auto. rewrite He3; auto. left; rewrite <- He1; auto. right; case H1; intros f (i, (Hf1, (Hf2, (Hf3, (Hf4, Hf5))))). exists f; exists i; repeat split; try rewrite <- He2; try rewrite <- He1; auto. rewrite <- He3; auto. apply iff_trans with (1 := Hs1 s); clear Hr1 Hs1 Ht1. apply iff_sym; apply iff_trans with (1 := Hs2 s); clear Hr2 Hs2 Ht2. split; intros [H1 | H1]; auto. left; rewrite He2; auto. right; case H1; intros f (i, (Hf1, (Hf2, (Hf3, (Hf4, Hf5))))). exists f; exists i; repeat split; try rewrite He2; try rewrite He1; auto. rewrite He3; auto. left; rewrite <- He2; auto. right; case H1; intros f (i, (Hf1, (Hf2, (Hf3, (Hf4, Hf5))))). exists f; exists i; repeat split; try rewrite <- He2; try rewrite <- He1; auto. rewrite <- He3; auto. apply iff_trans with (1 := Ht1 s); clear Hr1 Hs1 Ht1. apply iff_sym; apply iff_trans with (1 := Ht2 s); clear Hr2 Hs2 Ht2. split; intros [H1 | H1]; auto. left; rewrite He4; auto. right; case H1; intros f (i, (Hf1, (Hf2, (Hf3, (Hf4, Hf5))))). exists f; exists i; repeat split; try rewrite He2; try rewrite He1; auto. rewrite He3; auto. left; rewrite <- He4; auto. right; case H1; intros f (i, (Hf1, (Hf2, (Hf3, (Hf4, Hf5))))). exists f; exists i; repeat split; try rewrite <- He2; try rewrite <- He1; auto. rewrite <- He3; auto. Qed.
imports: ZArith List