proposition: Lemma all_equiv'_auxP : forall l n1 n2 d1 d2, l <> nil -> all_equiv'_aux l -> n1 < length l -> n2 < length l -> n1 <= n2 -> nth n1 l d1 -> nth n2 l d2.
proof: Proof. intro l; elim l; [intros ? ? ? ? H; exfalso; apply H; auto| clear l; intros a l _; revert a]. elim l; [intro a|clear l; intros b l IHl a]; intros n1 n2 d1 d2 _ H Hn1 Hn2 Hn. { simpl in Hn1, Hn2. apply PeanoNat.Nat.lt_1_r in Hn1; rewrite Hn1. apply PeanoNat.Nat.lt_1_r in Hn2; rewrite Hn2; simpl; auto. } { destruct H as [HI H]. revert dependent n2. revert dependent n1; intro n1. elim n1; [|clear n1; intros n1 IHn1]; intro Hn1. { intro n2; elim n2; [simpl; auto|clear n2; intros n2 IHn2 Hn2 _ Ha]. simpl in Ha; apply HI in Ha; apply IHl with 0 d1; auto; simpl in *; [discriminate|apply PeanoNat.Nat.lt_0_succ| apply Lt.lt_S_n; auto|apply le_0_n]. } { intro n2; elim n2; [intros _ HF; apply PeanoNat.Nat.nle_succ_0 in HF; intuition| clear n2; intros n2 IHn2 Hn2 HLe H']. assert (Hnth : forall n (l : list Prop) a d, nth (S n) (a :: l) d = nth n l d) by (intro n; induction n; simpl; auto). rewrite Hnth; rewrite Hnth in H'; clear Hnth; apply IHl with n1 d1; auto; [discriminate|simpl in Hn1|simpl in Hn2|apply Le.le_S_n]; auto; apply Lt.lt_S_n; auto. } } Qed.
imports: List