proposition: Lemma list_pred_eq_impl_eq : forall (A : Set)(ls1 ls2 : list A), list_pred eq ls1 ls2 -> ls1 = ls2.
proof: Proof. induction 1; intuition; simpl in *; subst. f_equal; eauto. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation