proposition: Lemma next2s_equiv p ps1 ps2 s : tequiv ps1 ps2 -> tequiv (next2s p ps1 s) (next2s p ps2 s).
proof: Proof. intros (H1, (H2, H3)). case (next2s_correct p ps1 s); intros Hr1 (Hs1, Ht1). case (next2s_correct p ps2 s); intros Hr2 (Hs2, Ht2). split; [idtac | split]; intros a. - apply iff_trans with (1:= (Hr1 a)); clear Hr1 Hs1 Ht1. apply iff_sym; apply iff_trans with (1:= (Hr2 a)); clear Hr2 Hs2 Ht2. split; intros [H4 | H4]. + left; case (H1 a); auto. + case H4; intros f1 (Hf1, (Hf2, (Hf3, Hf4))); right; exists f1; repeat split; auto; subst; case (H2 (f1 s)); auto. + left; case (H1 a); auto. + case H4; intros f1 (Hf1, (Hf2, (Hf3, Hf4))); right; exists f1; repeat split; auto; subst; case (H2 (f1 s)); auto. - apply iff_trans with (1:= (Hs1 a)); clear Hr1 Hs1 Ht1. apply iff_sym; apply iff_trans with (1:= (Hs2 a)); clear Hr2 Hs2 Ht2. split; intros [H4 | H4]. + left; case (H2 a); auto. + case H4; intros f1 (Hf1, (Hf2, (Hf3, Hf4))); right; exists f1; repeat split; auto; subst; case (H1 (f1 s)); auto. + left; case (H2 a); auto. + case H4; intros f1 (Hf1, (Hf2, (Hf3, Hf4))); right; exists f1; repeat split; auto; subst; case (H1 (f1 s)); auto. - apply iff_trans with (1:= (Ht1 a)); clear Hr1 Hs1 Ht1. apply iff_sym; apply iff_trans with (1:= (Ht2 a)); clear Hr2 Hs2 Ht2. split; intros [H4 | H4]. + left; case (H3 a); auto. + case H4; intros f1 (Hf1, (Hf2, (Hf3, Hf4))); right; exists f1; repeat split; auto; subst; case (H1 (f1 s)); case (H2 (f1 s)); auto. + left; case (H3 a); auto. + case H4; intros f1 (Hf1, (Hf2, (Hf3, Hf4))); right; exists f1; repeat split; auto; subst; case (H1 (f1 s)); case (H2 (f1 s)); auto. Qed.
imports: ZArith List