proposition: Theorem rZCompInvolList : forall L : list rZ, L = map rZComp (map rZComp L).
proof: Proof. intros L; elim L; simpl in |- *; auto with stalmarck. intros a l H'; rewrite <- H'; auto with datatypes stalmarck. rewrite <- rZCompInvol; auto with stalmarck. Qed.