proposition: Lemma all_equiv__equiv : forall l, all_equiv l <-> all_equiv' l.
proof: Proof. intro l; split. { elim l; [simpl; auto|clear l; intros a l _; revert a]. elim l; [simpl; intros; split; auto|clear l; intros b l _ a H; split]. { apply H; [apply in_eq|clear H; apply in_cons; revert b; revert a]. elim l; [simpl; auto|clear l; intros b l IHl d a]. assert (H : last (a :: b :: l) = last (b :: l)) by (induction l; simpl; auto); rewrite H; apply in_cons; auto. } { revert H; revert b; revert a; elim l; [|clear l; intros c l IHl a b H]; [simpl; intros a b H; split; auto; apply H; [apply in_cons|]; apply in_eq|]. split; [apply H; [apply in_cons|]; apply in_eq|]. apply IHl; intros x y Hx Hy; apply H; apply in_cons; auto. } } { elim l; [unfold all_equiv; simpl; tauto|clear l; intros a l _; revert a]. elim l;[ unfold all_equiv; simpl; intros a _ x y Hx Hy; elim Hx; [clear Hx; intro Hx|tauto]; elim Hy; [clear Hy; intro Hy|tauto]; rewrite <- Hx; rewrite Hy; tauto|clear l; intros b l _ a H]. intros x y Hx Hy; destruct H as [Hend Hbeg]. destruct (In_nth _ _ a Hx) as [n1 Hn1]; clear Hx; destruct Hn1 as [Hn1 Hx]. destruct (In_nth _ _ a Hy) as [n2 Hn2]; clear Hy; destruct Hn2 as [Hn2 Hy]. assert (Hlast : nth (S (length l)) (a :: b :: l) a = last (b :: l) a). { transitivity (nth (length l) (b :: l) a); [simpl; auto|]. revert dependent b. intros b _ _ _ _ _ _; clear n1 n2 x y. revert b; revert a; elim l; [simpl; auto|clear l; intros b l IHl d a]. transitivity (nth (S (length l)) (a :: b :: l) d); [simpl; auto|]. transitivity (nth (length l) (b :: l) d); [simpl; auto|]. rewrite IHl; simpl; auto. } assert (HaE : a = nth 0 (a :: b :: l) a) by (simpl; auto). rewrite <- Hlast in Hend; clear Hlast; rewrite <- Hx; rewrite <- Hy. elim (PeanoNat.Nat.lt_ge_cases n1 n2); intro HLe; split; try solve[apply all_equiv'_auxP; auto; try apply PeanoNat.Nat.lt_le_incl; auto; discriminate]; intro H; cut a; try (intro Ha; rewrite HaE in Ha; revert Ha); try(apply Hend; revert H); apply all_equiv'_auxP; auto; try discriminate; try apply PeanoNat.Nat.le_0_l; simpl in *; try apply PeanoNat.Nat.lt_0_succ; apply PeanoNat.Nat.lt_succ_r; auto. } Qed.
imports: List