proposition: Lemma ab_ba: forall n, repeat (a::b::nil) n == repeat (b::a::nil) n.
proof: Proof. intros; setoid_replace (a :: b :: nil) with (b :: a :: nil). - reflexivity. - repeat constructor. Qed.
imports: List Relation_Operators Operators_Properties Morphisms Setoid EMonoid