proposition: Lemma cons2_comm : forall d d' r, d::d'::r =r= d'::d::r.
proof: Proof. intros d d' r; change ((d::nil)++(d'::nil)++r =r= (d'::nil)++(d::nil)++r). do 2 rewrite app_assoc. rewrite (app_comm (d :: nil) (d'::nil));reflexivity. Qed.
imports: List ZArith Bool Relations Setoid Morphisms RelationClasses EMonoid Lia