proposition: Lemma nexts_equiv ps1 ps2 s : pequiv ps1 ps2 -> pequiv (nexts ps1 s) (nexts ps2 s).
proof: Proof. intros (H1, H2). case (nexts_correct ps1 s); intros Hr1 Hs1. case (nexts_correct ps2 s); intros Hr2 Hs2. split; intros a. - apply iff_trans with (1 := (Hr1 a)). apply iff_sym; apply iff_trans with (1:= (Hr2 a)). split; intros [H3 | H3]. + left; case (H1 a); auto. + case H3; intros f1 (Hf1, (Hf2, Hf3)); right; exists f1; repeat split; auto; unfold lequiv in H1; rewrite (H1 a); auto. + left; case (H1 a); auto. + case H3; intros f1 (Hf1, (Hf2, Hf3)); right; exists f1; repeat split; auto; intros H4; case Hf3; case (H1 a); auto. - apply iff_trans with (1 := (Hs1 a)). apply iff_sym; apply iff_trans with (1:= (Hs2 a)). split; intros [H3 | H3]. + left; case (H2 a); auto. + case H3; intros f1 (Hf1, (Hf2, Hf3)); right; exists f1; repeat split; auto; unfold lequiv in H1; rewrite (H1 a); auto. + left; case (H2 a); auto. + case H3; intros f1 (Hf1, (Hf2, Hf3)); right; exists f1; repeat split; auto; intros H4; case Hf3; case (H1 a); auto. Qed.
imports: ZArith List