proposition: Theorem iter_permutation: forall l1 l2, permutation l1 l2 -> iter l1 = iter l2.
proof: Proof. intros l1 l2 H; elim H; simpl; auto; clear H l1 l2. intros a l1 l2 H1 H2; apply f_equal2 with ( f := g ); auto. intros a b l; (repeat rewrite g_trans). apply f_equal2 with ( f := g ); auto. intros l1 l2 l3 H H0 H1 H2; apply trans_equal with ( 1 := H0 ); auto. Qed.
imports: List Permutation Arith